从一对到 lambda 演算/方案中的列表

Question

我正在学习一些关于 lambda 演算（非常简洁）的知识，并在方案中定义了以下如何完成一对：

; PAIR
; λabf.fab
(define PAIR (lambda (a) (lambda (b) (lambda (f) ((f a) b)))))
(define mypair ((PAIR 1) 2))

; FIRST
; λab.a
(define FIRST (lambda (a) (lambda (b) a)))

; SECOND
; λab.b
(define SECOND (lambda (a) (lambda (b) b)))

(display "First is: ")     (display (mypair FIRST))
(display " | Second is: ") (display (mypair SECOND))

First is: 1 | Second is: 2

如何进一步抽象这一点来创建一个列表的数据结构，例如，制作类似[1 2 3 4 5] 而不仅仅是[2 3] 的东西？

我自己能做的最好的事情就是对这些进行硬编码，例如，五个：

(define five (
    (PAIR 1) (
      (PAIR 2) (
        (PAIR 3) (
          (PAIR 4) 5)))))

(display (five FIRST)) (display ((five SECOND) FIRST)) (display (((five SECOND) SECOND) FIRST)) (display ((((five SECOND) SECOND) SECOND) FIRST)) (display ((((five SECOND) SECOND) SECOND) SECOND))

12345

对此有更“通用”的解决方案吗？

Answer 1

普通 LISP 列表不是[1 2 3]，而是(1 . (2 . (3 . ())))。它们是用 (cons 1 (cons 2 (cons 3 '()))) 创建的，所以 lambda 演算中的确切相等列表是 ((PAIR 1) ((PAIR 2) ((PAIR 3) ...)))

现在标准的 lisp 实现通常打印 (1 2 3)，但这是打印机完成的一些时髦的魔法。它的规则是，如果cdr 是一个列表，您可以省略点和一组括号。当您使用 lambda 演算对数据建模时，REPL 将始终显示 lambda/closure 对象，因此您需要了解结构并显示相应可视化的实用函数。这不是 lambda 演算的标准，因为它可以满足公理：

(car (cons a b)) ; ==> a
(cdr (cons a b)) ; ==> b

list 是cons 链接参数的辅助函数。你确实可以为对做类似的事情，但它不是 lambda 演算的一部分：

(define TRUE (lambda (p) (lambda (q) p)))
(define NIL (lambda (x) TRUE))

(define (ch-list . args)
  (let helper ((lst (reverse args)) (result NIL))
    (if (null? lst)
        result
        (helper (cdr lst)
                ((PAIR (car lst)) result)))))

Answer 2

正如西尔韦斯特所说。列表不是数组，它们是 conses 链，以特殊的 nil 或 () 对象结尾。这意味着要构建这样的东西，你需要cons 和这个特殊的对象。

我在 Racket 中实现了一种名为“oa”（一个参数）的玩具语言，在几分钟前，您可以找到 here。在其最纯粹的变体中，函数的语法是，例如(λ x x)：参数周围没有括号，因为为什么会有？ define 也可以给事物命名，但仅此而已。这是该语言的 conses 实现：

(define true (λ x (λ y x)))
(define false (λ x (λ y y)))

(define cons (λ h (λ t (λ s ((s h) t)))))
(define car (λ l (l true)))
(define cdr (λ l (l false)))
(define nil (λ l true))
(define null? (λ l (l (λ h (λ t false)))))

很方便（但也很烦人），oa 使用普通的 Racket 阅读器，因此您可以阅读数字，即使它们在语言中没有语义。所以，例如

> (cdr ((cons 1) 1))
1

例如，制作一个元素的三元素列表：

(define three-elt
  (λ e
    ((cons e)
     ((cons e)
      ((cons e)
       nil)))))

> (three-elt 1)
#<λ>
> (car (three-elt 1))
1
> (cdr (cdr (cdr (three-elt 1))))
{nil}: (λ l true)

（有一些特殊的、片状的、魔法可以让它打印出 defined 的事物的名称，就像在最后一个案例中一样。）

给定zero、zero?、succ 和pred（继任者和前任者）的定义，以及看起来像(((cond test) if-true) if-false) 的条件函数cond，然后您可以编写一个脏版本nth:

(define nth
  (λ n (λ c
         (((cond (zero? n))
           (car c))
          ((nth (pred n)) (cdr c))))))

这很脏，因为它免费使用nth，但您可以使用组合符来解决这个问题：我喜欢 U，所以：

(define U
  ;; The U combinator
  (λ f (f f)))

(define nth
  (U (λ t
       (λ n
         (λ c
           (((cond (zero? n))
             (car c))
            (((U t) (pred n)) (cdr c))))))))

使用以下任何一种：

> ((nth (succ zero)) ((cons true) ((cons false) nil)))
{false}: (λ x (λ y y))
> ((nth zero) ((cons true) ((cons false) nil)))
{true}: (λ x (λ y x))

我不认为你能做的是像这样实现list，因为即使你添加了特殊的魔法来表达像list 这样的nospread 函数，你也需要将它的所有参数变成一个列表。但我可能错了。

上述所有函数都存在于oa中的examples/lc.rkt中。