lisp - CLISP Lambda 微积分 Div 实现

Question

我正在尝试使用 clisp Lambda Calc 实现除法函数。风格

我读自this一个部门的 lambda 表达式是:

Y (λgqab. LT a b (PAIR q a) (g (SUCC q) (SUB a b) b)) 0

这些是正确的和错误的

(defvar TRUE #'(lambda(x)#'(lambda(y)x)))
(defvar FALSE #'(lambda(x)#'(lambda(y)y)))

这些是 Int 和 Church 数之间的转换函数

(defun church2int(numchurch)
    (funcall (funcall numchurch #'(lambda (x) (+ x 1))) 0)
)
(defun int2church(n)
    (cond
        ((= n 0) #'(lambda(f) #'(lambda(x)x)))
        (t #'(lambda(f) #'(lambda(x) (funcall f
            (funcall(funcall(int2church (- n 1))f)x))))))

)

这是我的 IF-THEN-ELSE 实现

(defvar IF-THEN-ELSE
    #'(lambda(c)
        #'(lambda(x)
            #'(lambda(y)
                #'(lambda(acc1)
                    #'(lambda (acc2)
                        (funcall (funcall (funcall (funcall c x) y) acc1) acc2))))))
)

这是我的div实现

(defvar division
    #'(lambda (g)
        #'(lambda (q)
            #'(lambda (a)
                #'(lambda (b)
                    (funcall (funcall (funcall (funcall (funcall IF-THEN-ELSE LT) a) b)
                        (funcall (funcall PAIR q)a))
                        (funcall (funcall g (funcall succ q)) (funcall (funcall sub a)b))
                    )))))

)

PAIR、SUCC 和 SUB 函数工作正常。我像这样设置我的教堂号码

(set six (int2church 6))
(set two (int2church 2))

然后我做:

(setq D (funcall (funcall division six) two))

我有:

#<FUNCTION :LAMBDA (A)
  #'(LAMBDA (B)
     (FUNCALL (FUNCALL (FUNCALL (FUNCALL (FUNCALL IF-THEN-ELSE LT) A) B) (FUNCALL (FUNCALL PAR Q) A))
      (FUNCALL (FUNCALL G (FUNCALL SUCC Q)) (FUNCALL (FUNCALL SUB A) B))))>

据我了解，此函数返回一个 Church Pair。如果我尝试获取第一个元素具有如下函数 FRST(FRST 工作正常):

(函数调用第一个 D)

我有

#<FUNCTION :LAMBDA (B)
  (FUNCALL (FUNCALL (FUNCALL (FUNCALL (FUNCALL IF-THEN-ELSE LT) A) B) (FUNCALL (FUNCALL PAR Q) A))
   (FUNCALL (FUNCALL G (FUNCALL SUCC Q)) (FUNCALL (FUNCALL SUB A) B)))>

如果我像这样尝试使用 Church2int 获取 int 值(Church2int 工作正常):

(church2int (funcall frst D))

我有

*** - +:
       #<FUNCTION :LAMBDA (N)
         #'(LAMBDA (F)
            #'(LAMBDA (X)
               (FUNCALL (FUNCALL (FUNCALL N #'(LAMBDA (G) #'(LAMBDA (H) (FUNCALL H (FUNCALL G F))))) #'(LAMBDA (U) X)) (LAMBDA (U) U))))>
      is not a number

我希望得到 3

我认为问题出在 DIVISION 函数中，在 IF-THEN-ELSE 之后，我试图稍微更改它(我认为这是一个嵌套的括号问题)但是我得到了很多错误。

任何帮助将不胜感激

谢谢

Answer 1

你的定义有几个问题。

DIVISION 不使用 Y 组合子，但原始定义使用。这很重要，因为 DIVISION 函数需要在 g 中有一个它自己的副本参数。

但是，即使您添加了 Y 调用，您的代码仍然无法运行而是进入无限循环。这是因为 Common Lisp 与当今的大多数语言一样，是一种按值调用的语言。在调用函数之前评估所有参数。这意味着您无法像传统的 lambda 演算语义所允许的那样优雅地定义条件函数。

这是在 Common Lisp 中进行教堂编号除法的一种方法。我冒昧地引入了一些语法来提高可读性。

;;;; -*- coding: utf-8 -*-
;;;; --- preamble, define lambda calculus language

(cl:in-package #:cl-user)

(defpackage #:lambda-calc
  ;; note: not using common-lisp package
  (:use)
  (:export #:λ #:call #:define))

;; (lambda-calc:λ (x y) body)
;;   ==> (cl:lambda (x) (cl:lambda (y) body))
(defmacro lambda-calc:λ ((arg &rest more-args) body-expr)
  (labels ((rec (args)
             (if (null args)
               body-expr
               `(lambda (,(car args))
                  (declare (ignorable ,(car args)))
                  ,(rec (cdr args))))))
    (rec (cons arg more-args))))

;; (lambda-calc:call f a b)
;;   ==> (cl:funcall (cl:funcall f a) b)
(defmacro lambda-calc:call (func &rest args)
  (labels ((rec (args)
             (if (null args)
               func
               `(funcall ,(rec (cdr args)) ,(car args)))))
    (rec (reverse args))))

;; Defines top-level lexical variables
(defmacro lambda-calc:define (name value)
  (let ((vname (gensym (princ-to-string name))))
    `(progn
       (defparameter ,vname nil)
       (define-symbol-macro ,name ,vname)
       (setf ,name
             (flet ((,vname () ,value))
               (,vname))))))

;; Syntax: {f a b}
;;   ==> (lambda-calc:call f a b)
;;   ==> (cl:funcall (cl:funcall f a) b)
(eval-when (:compile-toplevel :load-toplevel :execute)
  (set-macro-character #\{
                       (lambda (stream char)
                         (declare (ignore char))
                         `(lambda-calc:call
                            ,@(read-delimited-list #\} stream t))))
  (set-macro-character #\} (get-macro-character #\))))

;;;; --- end of preamble, fun starts here

(in-package #:lambda-calc)

;; booleans
(define TRUE
  (λ (x y) x))
(define FALSE
  (λ (x y) y))
(define NOT
  (λ (bool) {bool FALSE TRUE}))

;; numbers
(define ZERO
  (λ (f x) x))
(define SUCC
  (λ (n f x) {f {n f x}}))
(define PLUS
  (λ (m n) {m SUCC n}))
(define PRED
  (λ (n f x)
    {n (λ (g h) {h {g f}})
       (λ (u) x)
       (λ (u) u)}))
(define SUB
  (λ (m n) {n PRED m}))

(define ISZERO
  (λ (n) {n (λ (x) FALSE) TRUE}))
(define <=
  (λ (m n) {ISZERO {SUB m n}}))
(define <
  (λ (m n) {NOT {<= n m}}))

(define ONE   {SUCC ZERO})
(define TWO   {SUCC ONE})
(define THREE {SUCC TWO})
(define FOUR  {SUCC THREE})
(define FIVE  {SUCC FOUR})
(define SIX   {SUCC FIVE})
(define SEVEN {SUCC SIX})
(define EIGHT {SUCC SEVEN})
(define NINE  {SUCC EIGHT})
(define TEN   {SUCC NINE})

;; combinators
(define Y
  (λ (f)
    {(λ (rec arg) {f {rec rec} arg})
     (λ (rec arg) {f {rec rec} arg})}))

(define IF
  (λ (condition if-true if-false)
    {{condition if-true if-false} condition}))

;; pairs
(define PAIR
  (λ (x y select) {select x y}))
(define FIRST
  (λ (pair) {pair TRUE}))
(define SECOND
  (λ (pair) {pair FALSE}))

;; conversion from/to lisp integers
(cl:defun int-to-church (number)
  (cl:if (cl:zerop number)
    zero
    {succ (int-to-church (cl:1- number))}))
(cl:defun church-to-int (church-number)
  {church-number #'cl:1+ 0})

;; what we're all here for
(define DIVISION
  {Y (λ (recurse q a b)
       {IF {< a b}
           (λ (c) {PAIR q a})
           (λ (c) {recurse {SUCC q} {SUB a b} b})})
     ZERO})

如果将其放入文件中，您可以:

[1]> (load "lambdacalc.lisp")
;; Loading file lambdacalc.lisp ...
;; Loaded file lambdacalc.lisp
T
[2]> (in-package :lambda-calc)
#<PACKAGE LAMBDA-CALC>
LAMBDA-CALC[3]> (church-to-int {FIRST {DIVISION TEN FIVE}})
2
LAMBDA-CALC[4]> (church-to-int {SECOND {DIVISION TEN FIVE}})
0
LAMBDA-CALC[5]> (church-to-int {FIRST {DIVISION TEN FOUR}})
2
LAMBDA-CALC[6]> (church-to-int {SECOND {DIVISION TEN FOUR}})
2