题目来自 functional，发售于 Steam (29 CNY).

Basic

anything

写出任意一个符合 Lambda Calculus 语法 (1. variable 2. abstraction 3. application) 的 term 即可.

identity

x: x

two arguments

x:y: y x

squaring

f:x: f (f x) 

indirection

f:x:y: f y x

Boolean

定义：

TRUE = t:f: t
FALSE = t:f: f

IF

p:t:f: p t f

Simple LC 没有类型系统，所以编程者需要自己确保 p 一定能求值到 TRUE / FALSE，然后 p t f 进一步求值到 t/ f，如果 p 不能被求值到 TRUE / FALSE，那么 p t f 会被保留下来或者产生预期外的求值行为.

你可以轻松注意到的一点是：IF P A B ≡ P A B，你完全可以在所有使用 IF 的场合省略掉 IF，这不改变语义，同时可以减少一次 reduction，不过为了保证可读性，还是有理由在有点复杂的程序里保留 IF.

NOT

b: b FALSE TRUE

这个看着有点隐隐约约的巧妙. 可以直白地通过 b: IF b FALSE TRUE → b FALSE TRUE 得到，或者利用 TRUE / FALSE 的意义——选第一个 / 第二个——直接得到.

AND

p:q: p q p

如果 p = TRUE，那么 AND p q ≡ q；如果 p = FALSE，那么 AND p q ≡ FALSE ≡ p.

OR

p:q: p p q

如果 p = TRUE，那么 OR p q ≡ p ≡ TRUE；如果 p = FALSE，那么 OR p q ≡ q.

XOR

p:q: p (NOT q) q

类似 AND, OR，可以画个真值表整理思绪.

Pair and List

PAIR

x:y:f: f x y

PAIR A B → (x:y:f: f x y) A B → (f: f A B) 是一个这样的抽象：有序地内涵 A, B，等待一个函数 f 作用于内涵的 A, B，比如当 A, B 是 Boolean，那么，f 可以是 AND / OR / …（当然语法并不约束 f,A,B 的形状，如果你想写 PAIR TRUE 0 PAIR 解释器不会拦你）

FST

p: p TRUE

当 p = PAIR A B 时, p TRUE → (PAIR A B) TRUE → (f: f A B) TRUE → TRUE A B → A，注意 p 是一个可以接收一个参数 f 的函数，这里我们让它接收 TRUE 函数来选取第一个元素. 在 LC 里，TRUE / FALSE 更恰当的解释是选取其后跟随的第一 / 二个项，而不是表达某个命题的真 / 假，这是有意义的，因为我们写其他高级语言程序的时候，如果我们需要一个 Boolean 值 X ，X 最终的效用往往还是发挥在 then-clause / else-clause 的选择上.

SND

p: p FALSE

类似 FST.

simple list

取出列表的第 3 项 (1-indexed)：

l: FST ( SND ( SND l ) )

列表是一种简单的递归结构，递归基是空列表，这里用 FALSE 表示，递归步是向某个列表添加元素，这里用 PAIR 实现，e.g. [] ↦ FALSE, 1 ↦ (PAIR 1 FALSE), [1,3] ↦ (PAIR 1 (PAIR 3 FALSE))，注意 [1,3]的例子，如果从向列表添加元素的视角看，表头是最接近 FALSE 的项，越接近 FALSE 的元素索引越小，因为它比较早地被添加进来，在这种解释下，[1,3] ↦ (PAIR 3 (PAIR 1 FALSE))，然而游戏里不采取这个解释，而是和我们熟悉的 [a,b,..] 保持视觉上的对齐，将最晚被添加的项——最左的项——作为表头，在后续涉及升降序的问题的时候记得留意这一点.

ANY

对一个含 3 个 Boolean 的列表，若任一项为 TRUE，返回 TRUE，否则返回 FALSE：

(l: IF 
    (OR 
        (FST (SND (SND l))) 
        (OR 
            (FST l) 
            (FST (SND l))
        )
    )
    TRUE FALSE
)

直白地按逻辑写即可. 这里的列表是定长的，比较方便，非定长列表就需要递归，见后.

PUSH

(m:l: PAIR m l)

用 PUSH 向列表 l 添加新项 m，根据 $\eta$-reduction，PUSH ≡ PAIR，所以这里直接写 PAIR 也足够了.

POP

SND

弹出最外层的项.

EMPTY

l: l (t:x:y: FALSE) TRUE

首先 EMPTY 要接收一个列表，所以它的基本形状是 EMPTY = l: ...，考虑 l' = FALSE 的情形，EMPTY l' ~ᴇxᴘᴇᴄᴛᴇᴅ→ TRUE，根据 FALSE 的选择能力，我们使 EMPTY = l: l 𝕏 TRUE；考虑 l* = PAIR a (PAIR b (...)) = (f: f a (PAIR b (...))) ≈ (f: f a _tail)，把 l* 视作接收一个参数的函数，EMPTY l* = (f: f a _tail) 𝕏 TRUE → 𝕏 a _tail TRUE ~ᴇxᴘᴇᴄᴛᴇᴅ→ FALSE, 那么 𝕏 的工作就是接收后面的 3 项，然后返回 FALSE，所以 𝕏 = (t:x:y: FALSE)，综合以上得到最终的解 EMPTY = l: l (t:x:y: FALSE) TRUE

Recursion

create recursion - Y combinator

动机：LC 中的递归

尝试着在 LC 中定义递归的阶乘函数：

f = a: IF (EQ a 1)
       1
       (a * f (a - 1))

上述的定义是不符合 LC 的语法的，因为 LC 的函数都是匿名函数，不支持通过名称来调用函数（如上面的 f），而递归函数不可避免的需要自指，如何解决这个问题？

将函数 $F$ 应用于参数 $A$，可以这样表达 $F A$，也可以利用高阶函数这样表达：$(\lambda fa.\ f\ a) F A$，在此基础上，添加一些逻辑，比如表达"参数为 $a$ 和 $p$，函数为 $f$，若 $p\ a$ 为真，那么返回 $f\ a$，否则直接返回 $a$ 本身"：$(\lambda fap.\ IF\ (p\ a)\ (f\ a)\ a)$. 根据这个想法，假设我们的目标阶乘函数为 F，那么 F 满足这个等式，将 (f:a: ..) 记作 F'：

F = (f:a: IF (EQ a 1)
          1 
          (a * f (a - 1))
    )  F 
  ≡ F' F 

看等式的右侧，F' 的涵义是，接收函数 f 和参数 a，若 EQ a 1 那么返回 1，否则返回返回 a * f (a - 1). 向 F' 传递递归函数 F，由此得到的函数 F' F 的行为和我们目标的阶乘函数 F 是一致的，从语义上来讲，左右侧相等.

目前我们有的等式是 F = F' F ①，其中 F' 是已知的 closed term，因为 F 涉及自引，所以不存在 normal form，于是考虑是否存在某个 Y s.t. Y F' = F②，将 ② 代入 ①，Y F' = F' (Y F')，接下来的目标就是解出 Y 的 normal form，得到 Y 之后，目标递归函数 F = Y F' 也随之得到了.

Y combinator 设计

Y 是一个这样的 term：Y F = F (Y F) = F (F (Y F)) = .... （注意：是否持续展开取决于我们使用的求值策略）

为设计满足以上目标的 Y ，做出如下的初步分析：

1. Y 的形状毫无疑问是 (f: ...).

2. Y 的自指？—— 我们需要重复 Y，或者说构建右侧的 Y.

   Function / Abstraction is All You Need —— 因为 LC 没有存储，所以 Y F = F (Y F)，等号左右的 Y 并不是同一个 Y，不是值拷贝或者地址拷贝（因为 LC 不提供存储的概念，无处安放值或者地址，这里只有函数），右侧的 Y 需要通过构建得到，与左侧的 Y 在 alpha-conversion 的意义下相等.

3. 如何重复 F？这很简单，Y = (f: ...) 接收参数 F，在 Y 的函数体内，想怎么重复就怎么重复.

4. 设计一个 abstraction M 做构建，M 将接收一些必要的参数，在函数体内组织这些参数，形成和 Y 一样的结构.

   1. Y = f: M f ... ~ᴇxᴘᴇᴄᴛᴇᴅ→ M = f: f (Wai f)：毫无疑问，M 需要拿到 Y 的参数 f，M 内部需要建立起和 Y F 一致的结构；
   2. Y = f: M f M ... ~ᴇxᴘᴇᴄᴛᴇᴅ→ M = f:m: f (m f m)：因为我们希望 M 可以建立起和 Y F 一致的结构，而 Y 包含了 M，那么 M 也需要包含 M，所以通过参数 m 将 M 原封不动地传进 M. M 的函数体中，最左的 f 实现 f 的再次应用，(m f m) 构建了和左侧的 Y F alpha 等价的结构.
   3. Y = f: M f M, 其中 M = f:m: f (m f m)，可以验证这已经是一个可行的 Y 组合子了，Y F = M F M = (f:m: f (m f m)) F M = F (M F M) = F (M F M) = F (Y F).

5. Y 组合子可以有无数种，比如 (a) Y = f: M M f, M = m:f: f (m m f) 这和上文所呈现的 Y 组合子是几乎一样的，只是改变了 M, f 参数的顺序，利用一步 $\eta$ 规约，使之更简洁——Y = M M, M = ...，这也是图灵给出的 Y 组合子；(b) Y = f: E (E f) E f, E = r:s:f: f (s r s f) 也是可以的，看起来不够简洁，但是理念和上面的陈述是一致的，用 E 接收需要知道的参数，然后做构建，你会发现 E 接收了 E 和 f，又多余地接收了 (E f)，把 (E f) 拿掉并做相应的修改，就得到了本段落陈述的第一种 Y 组合子；(c) 最简洁的 Y = f: (x: f (x x)) (x: f (x x))，它和前面提到的 Y 组合子的区别在于，前面的 Y 组合子是用组合子组成的，比如 4 中的 Y = f: M f M 中的 M 本身也是组合子，而这个 Y 组合子不包含组合子子项.

• 小练习：如何实现满足双边延展的 D F D = D (D F D) D = ... 的组合子 D？

  一种解法可以是 D = f:d: d (d f d) d，道理和之前所说的是一致的.

• Y 一定要是组合子吗，可以引入自由变量吗？

  假设 Y 包含自由变量 z，因为 Y 包含 z，那么用 M 构建 Y 时也要考虑到 z：

  1. closed M：将 z 作为参数传给 M，那么可以在之前的 Y 组合子的基础上修改，得到 Y = f: M f c M, M = f:c:m: f (m f c m)，可以验证，这可以达成 Y F = F (Y F) = ... 的目标，同时你可以注意到引入 z 并没有什么意义，只是平添负担;
  2. open M：即 M 本身包含了自由 z，可以尝试 Y = f: K f K z, K = f:k: f (k f k z)这个例子，你会发现这是行不通的： Y F = F (K F K z) z = F (Y F) z = F (F (Y F) z) z，这个 Y 的效果是在左侧不断做 F 的应用，右侧不断产生新的 z.

  根据以上的讨论，这个问题的答案是：可以，但没必要. 且从直觉上去理解，随意地引入自由变量也没有意义. 我提出这个问题的原因是，有一瞬间突然觉得 Y 组合子太熟悉了，第一次在 LC 里见到 Y 这个大写字母后面接的就是"组合子"三个字，所以开始考虑，如果不是组合子是否可以.

Y combinator 使用

承接动机部分，我们用 F' = f:a: ... 表达递归函数 f 与其参数 a 之间的应用逻辑，将目标递归函数为 F，那么 F = F' F，因为自引的不合法，考虑用 Y F' 来表示 F，在上一节中我们涉及出了可行的 Y，于是 F = Y F' 就是我们希望得到的目标函数.

想明白 Y 组合子的使用，本 section 的关卡都很简单了，唯一值得提示的是 1. 使用以往关卡已定义过的函数时，注意函数的参数顺序，例如 FILTER 先传列表，再传过滤依赖的函数，因为 Simple LC 语法层面的约束很少，所以编程者自己要多当心一些 2. 有若干个关卡可能涉及列表反转，所以 REVERSE 可以先写，然后直接拿来用 3. 注意括号配对，可以现在先进的编辑器里先写，确保不犯低级错误，再复制进来评测. 下面给出的答案仅供参考，可以过评测，但未必最简.

strip prefix

去除不定长列表前缀的 FALSE：

Y (f:l:
      IF 
      (FST l)
      l 
      (f (SND l))
  )

ACC

Y  (a:l:f:i: 
      IF (EMPTY l)
      i 
      (a (SND l) f (f i (FST l))) 
   )

ALL

l: ACC l AND TRUE

REVERSE

Y (i:c:l: 
    IF 
      (EMPTY l) 
      c 
      (i (PAIR (FST l) c) (SND l))
  ) 
  FALSE 

MAP

Y  (m:c:l:f:
        IF 
        (EMPTY l)
        (REVERSE c)
        (m (PAIR (f (FST l)) c)  (SND l) f) 
    )
FALSE

NONE

(l: ALL (MAP l NOT))

FILTER

Y (m:c:l:f:
        IF 
        (EMPTY l)
        (REVERSE c)
        (   IF 
            (f (FST l))
            (m (PAIR (FST l) c) (SND l) f) 
            (m c (SND l) f)
        )
  )
  FALSE

ZIP

Y (z:c:m:n:
    IF 
    (EMPTY m)
    (REVERSE c)    
    (z (PAIR (PAIR (FST m) (FST n)) c) (SND m) (SND n)) 
  ) 
  FALSE

EQBLIST

(m:n: ALL 
      (MAP 
         (MAP 
            (ZIP m n) 
            (p: XOR (FST p) (SND p))
         ) 
         NOT
      ) 
)

CONCAT

(m:n: 
    (Y (g:c:r:
        IF (EMPTY r)
        c
        (g (PAIR (FST r) c) (SND r))
       )
    )
    n (REVERSE m) 
)

Numerals

Church Numeral 用函数表达自然数，两个关键点是 1. 基 (0 := f:x: x) 2. 后继 (SUC)，在基之上不断做后继，就可以得到所有 Church Numeral.

SUC

给定 Church Numeral n，n 是一个函数，参数为 f, x，n f x 表示将 f 应用于 x $n$ 次，SUC n 是一个函数，这个函数的能力是接收 f, x，将 f 应用于 x $(n+1)$ 次.

(n: (f:x: f (n f x) ) )

ZERO

利用逻辑运算来判断给定的 n 是不是 f:x: x.

(n: n (x: AND FALSE x) TRUE)

PRE

一个基本的观察是 n = n SUC 0，这里的等号表示内涵等价（intensional equality），那么在 PAIR 0 0 上做 $n$ 次迭代，一轮迭代的工作是：1. 右侧数对齐左侧数 2. 左侧数做一次后继，那么右侧数始终慢左侧数一步，即 $n$ 轮迭代后，左侧数是 n，右侧数是左侧数的后继.

(n: SND (n (p: PAIR (SUC (FST p)) (FST p)) (PAIR 0 0) ) )

ADD

给定 x, y，目标是给出 x+y，x+y 的含义是：预备接收 f, z，将 f 应用于 z $(x+y)$ 次. 先将 f 应用于 z $x$ 次，得到结果 x f z，再将 f 应用于 (x f z) $y$ 次.

(x:y: (f:z: y f (x f z)) )

SUB

(x:y: (f:z: (y PRE x) f z))

MUL

(x:y:f:z: y (x f) z )

DIV

(Y (d:c:x:y:
        IF (ZERO x)
        0    
        ( 
          IF (ZERO (y PRE x))
          (SUC c)
          (d (SUC c) (y PRE x) y)
        ) 
   ) 
) 0

EQ

(x:y: AND 
        (ZERO (x PRE y)) 
        (ZERO (y PRE x))
)

MIN

(x:y: IF (ZERO (x PRE y))
      y
      x
)

MAX

(x:y: IF (ZERO (x PRE y))
      x
      y
)

More Numerals

is odd

(n: (n NOT FALSE))

顺便想起了判断奇偶的递归方法：（看起来还挺有意思的，比熟悉的 mod 2 新鲜一些）

isEven :: Int -> Bool 
isEven 0 = True 
isEven x = isOdd (x-1)

isOdd :: Int -> Bool
isOdd 0 = False
isOdd x = isEven (x-1)

increasing list

尾递归：

(Y (f:c:n: IF (ZERO n)
           (PAIR 0 c)
           (f (PAIR n c) (PRE n))
   ) 
) FALSE

非尾递归：

(n: REVERSE 
    ( 
     (Y (f:x: 
            IF (ZERO x)
            (PAIR 0 FALSE)
            (PAIR x (f (PRE x))))
     ) n
    )
)

decomposition

将给定数分解成 2 的幂之和：

(Y (f:c:k:n:
     IF (ZERO n)
     c
     (IF (AND (EQ n (MIN k n)) (NOT (EQ k n)))  
         (f c (DIV k 2) n)
         (f (PAIR k c) (DIV k 2) (SUB n k) )
     )
   )
) FALSE 8

* primes 和 sort 都需要大把时间运行（本机测试两关各自耗时都在 30min 左右）

primes

Y (f:l:p:n: 
     IF (EQ n (FST p)) 
     (PAIR n l)
     (IF (EQ (FST p) (MAX n (FST p)))
      (f l (SND p) n)
      ( IF (
            (Y (f:n:p:
                IF (EQ n (MIN n p) )
                (IF (EQ n p) TRUE FALSE )
                (f (SUB n p) p)   
               )
            ) n (FST p)
           )
        (f (PAIR (FST p) l) p (DIV n (FST p)))
        (f l (SND p) n)
      )
     )
  )
  FALSE
  (PAIR 47 (PAIR 43 (PAIR 41 (PAIR 37 (PAIR 31 (PAIR 29 
  (PAIR 23 (PAIR 19 (PAIR 17 (PAIR 13 (PAIR 11 (PAIR 7 
  (PAIR 3  (PAIR 2 FALSE))))))))))))))

sort

选择排序：

Y (f:c:l: 
    IF (EMPTY l)
    c
    (
        (m: (f (PAIR m c) (FILTER l (x: NOT (EQ x m)) )) ) 
        (ACC l MAX 0)
    )
  ) FALSE

trees

NODE

l:v:r:f: f l v r

LEF

t: t (l:v:r: l) 

RIG

t: t (l:v:r: r)

VAL

t: t (l:v:r: v)

BEMPTY

类似于列表判空，NODE l v r = f: f l v r，空树用 FALSE := a:b: b 表示，将一个树 t 作为函数使用，若是空树，t A B = FALSE A B = B ~ᴇxᴘᴇᴄᴛᴇᴅ→ TRUE，若不是空树 t A B = (f: f l v r) A B = A l v r B ~ᴇxᴘᴇᴄᴛᴇᴅ→ FALSE，根据以上，B = TRUE, A = l:v:r:x FALSE，所以：

(t: t (l:v:r:x: FALSE) TRUE )

FIND

判断树 t 中是否存在值为 v 的结点：

Y (f:t:v:
    IF (BEMPTY t)
    FALSE
    (IF (EQ (VAL t) v)
     TRUE
     (OR (f (LEF t) v) (f (RIG t) v))    
    )
  )

BSIZE

计算树的规模：

Y (f:t:
    IF (BEMPTY t)
    0
    (SUC (ADD (f (LEF t)) (f (RIG t))))
  )

BUILD

二叉搜索树的构造：

Y (f:c:l:
    IF (EMPTY l)
    c
    (   f
        (
          (
          Y (f:v:t:
              IF (BEMPTY t)
              (NODE FALSE v FALSE)
              ( IF (EQ v (MIN v (VAL t)))
                (NODE (f v (LEF t)) (VAL t) (RIG t))
                (NODE (LEF t) (VAL t) (f v (RIG t)))
              )
            )
          )           
          (FST l) c)
        (SND l)
    ) 
  ) FALSE

[ 游戏里的 PREORDER 和 INORDER 两个函数似乎反了？ ]

PREORDER

二叉树的中序遍历：

Y (f:t: 
    IF (BEMPTY t)
    FALSE
    (CONCAT (f (LEF t))
        (PUSH (VAL t)  
              (f (RIG t))
        )
    )
  )

INORDER

二叉树的前序遍历：

Y (f:t: 
    IF (BEMPTY t)
    FALSE
    (PUSH (VAL t)
        (CONCAT (f (LEF t)) 
                (f (RIG t))
        )
    )
  )

SPLIT

树 t 以 v 为界进行分割：

Y (f:t:v:
    IF (BEMPTY t)
    (PAIR FALSE FALSE)
    (
      IF (EQ v (MAX v (VAL t)))
      (
        (p: PAIR (NODE (LEF t) (VAL t) (FST p)) (SND p)) 
        (f (RIG t) v)
      )
      (
        (p: (PAIR (FST p) (NODE (SND p) (VAL t) (RIG t) ))) 
        (f (LEF t) v)
      )
    )
  )

KTH

对给定的二叉搜索树，给出其中第 k 大的元素，取出树的中序遍历列表中的第 k 项即可：

(t:k: 
    Y (f:c:l:
        IF (EQ c 0)
        (FST l)
        (f (PRE c) (SND l) )
    ) k (PREORDER t)
)

inverse 6

对给定的二叉搜索树 t，找出 [1..6] 中的若干个缺席者，升序排列：

t: 
  IF (BEMPTY t)
  (PAIR 1 (PAIR 2 (PAIR 3 (PAIR 4 (PAIR 5 (PAIR 6 FALSE))))))
  (
   Y (f:c:m:n:
        IF (EMPTY n)
        (REVERSE c)
        (
          IF (EQ (FST m) (FST n))
          (f c (SND m) (SND n))
          (f (PAIR (FST n) c) m (SND n))
        )
    ) 
    FALSE
    (PREORDER t)
    (PAIR 1 (PAIR 2 (PAIR 3 (PAIR 4 (PAIR 5 (PAIR 6 FALSE))))))
  )