Fixpoint is all you need

A little bondage is always a good thing.

Origin: the duplicating name

若无说明，我们使用 CBN，而非 CBV. 即我们总是惰性求值的。

• 这就产生了问题：如果约束变量和自由变量重名会怎么样。

Bound Substitution

Accidental Capturing

insights

Combinator Defined

Preliminary

• 所以说组合子通过消灭变量的约束与自由之区别解决了重名问题——大家（指变量）的地位都一样。

吉祥三宝

• I 即 Identity（应该吧？Schönfinkel 是德国人，不好说），返回自身。

• K 即 Konstant（应该吧？），输入一个 x 则得到一个返回 x 的常函数，接着再输入一个 y 就能得到 x。（lambda calculus 中只有一元函数，相当于 currying），也可以看成 K 返回一个2-元组的第一个元素。

• S 即 Substitute（应该吧？），即 apply x to y. 但这个 Application 是 generalized 的：x, y 是在 z 下（所以 x, y 首先应用于 z）进行运算的。可以把 z 看成一个环境（environment）。例如 .

• 显然，combinator 本质上是 higher-order function. This is what combinator logic is all about.

Duplicator

• 如果是 call-by-value/eager eval，会首先去求解 ，显然 M 永远求不出值，程序也就不能终止。

• 如果是 call-by-name，会首先将 M 代入式子中，最后计算，显然值为 1.

Combinatory Logic

Combinatory logic (henceforth: CL) is an elegant and powerful logical theory that is connected to many areas of logic, and has found applications in other disciplines, especially, in computer science and mathematics.

https://plato.stanford.edu/entries/logic-combinatory/index.html

Recursion Implemented

Factorial

def fact: ℕ -> ℕ
  | 0 => 1
  | n + 1 => (n + 1) * fact n

(defun fact (n) (if (zerop n) 1 (* n (fact (1- n)))))

• 因此我们实际上是要构造一个 lambda 项 fact 使得其满足上面这一等式。

• 换句话说，递归方程的解是该方程对应的函数的一个不动点。

• 长得像 fact 但不是 fact ——根据其作用，不妨称其为 cons-fact 吧，即 fact 构造子。

Attracting Fixed Points

• 但这也不够好——我们想从头构造出 fact 来。而程序需要终止——对于收敛于不动点的无穷序列来说，程序终止的那一刻我们只能获得一个近似，而非 fact 本身。

• 那么有没有办法构造出不动点 fact 本身呢？也许我们需要改写 了。

Recursion by Self-Application

真是条条大路通罗马呀（万常选等. 数据库系统原理与实践）

Y

1. 构造了一个函数 ，描述了某个递归定义，接着我们要寻找它的不动点

2. 于是我们构造了

3. 接着我们求一步 ：

Alternate Y

Implementation Restrictions

#lang lazy

(define Y (λ (f) ((λ (x) (f (x x))) (λ (x) (f (x x))))))

(define fact
  (Y (λ (fact) (λ (n) (if (zero? n) 1 (* n (fact (- n 1))))))))

1. 静态类型语言不能很好地处理递归类型（ 可能没有 finite type）（我们上面讨论的是动态类型的 lambda calculus/ Unityped LC）严格来说不算问题。

2. CBV （计算 时先求 ，而不是先代入，不能终止）——会爆栈

Z

arguments to functions are evaluated before the function is applied.

• compare to that of CBN:

• 这个问题是我初学时遇到的，却没见什么人讲。

• 理论上，现在我们也能在 CBV 中使用递归了—— 直接把定义翻译成代码试试。

(defun Y (f) ; actually it's `Z`
  ((lambda (x)
     (funcall f (lambda (y)
                  (funcall (funcall x x) y))))
   (lambda (x)
     (funcall f (lambda (y)
                  (funcall (funcall x x) y))))))

(defun cons-fact (f) ; T
  (lambda (n)
    (if (zerop n)
        1
        (* n (funcall f (1- n))))))

(defun cons-ackermann (f)
  (lambda (m n)
    (cond
     ((zerop m) (1+ n))
     ((and (> m 0) (zerop n)) (funcall f (1- m) 1))
     ((and (> m 0) (zerop n)) (funcall f (1- m) (funcall f m (1- n)))))))

(funcall (Y #'cons-fact) 4) ; => 24
(mapcar (Y #'cons-fact) '(0 1 2 3 4 5 6 7 8 9 10))
; => (1 1 2 6 24 120 720 5040 40320 362880 3628800)

(defun fact (n)
  (if (zerop n)
      1
      (* n (fact (1- n)))))

(defun tfact (n &optional (acc 1)) ; tail-recursive
  (if (zerop n)
      acc
      (tfact (1- n) (* n acc))))

(defun ffact (n)
  (reduce #'* (iota n))) ; any sane person would do

(mapcar (lambda (f) (time (funcall f 20000)))
    `(,#'fact ,#'tfact ,#'ffact ,(Y #'cons-fact)))

;; Order: fact -> tfact -> ffact -> (Y #'cons-fact)
Evaluation took:
  0.057 seconds of real time
  0.104721 seconds of total run time (0.092086 user, 0.012635 system)
  [ Real times consist of 0.003 seconds GC time, and 0.054 seconds non-GC time. ]
  [ Run times consist of 0.003 seconds GC time, and 0.102 seconds non-GC time. ]
  184.21% CPU
  332,241,824 bytes consed
  
Evaluation took:
  0.064 seconds of real time
  0.062912 seconds of total run time (0.053324 user, 0.009588 system)
  [ Real times consist of 0.015 seconds GC time, and 0.049 seconds non-GC time. ]
  [ Run times consist of 0.015 seconds GC time, and 0.048 seconds non-GC time. ]
  98.44% CPU
  339,602,176 bytes consed
  
Evaluation took:
  0.060 seconds of real time
  0.059242 seconds of total run time (0.038523 user, 0.020719 system)
  98.33% CPU
  303,779,168 bytes consed
  
Evaluation took:
  0.061 seconds of real time
  0.060913 seconds of total run time (0.041709 user, 0.019204 system)
  [ Real times consist of 0.002 seconds GC time, and 0.059 seconds non-GC time. ]
  [ Run times consist of 0.001 seconds GC time, and 0.060 seconds non-GC time. ]
  100.00% CPU
  304,801,856 bytes consed

• Y combinator 的效率是很低效的。不如说整个 Church Encoding 都是。

(defun Y (f)
  ((lambda (x) ; W
     (funcall f (lambda (y)
                  (funcall (funcall x x) y))))
   (lambda (x)
     (funcall f (lambda (y) ; W
                  (funcall (funcall x x) y))))))

(defun Y (f)
  ((lambda (x) ;; M
     (funcall x x))
   (lambda (x) (funcall f ;; W
                 (lambda (y)
                   (funcall (funcall x x) y))))))

(defun Y (f) (lambda (x) (funcall (funcall f (Y f)) x))) ; Y f = f (Y f)

• 对任何的 unityped/untyped(in the sense of not statically typed) language 来说， 都是可以轻松实现的。

The Y combinator can be implemented indirectly using, for example, the linear representations of verbs (Y becomes a wrapper which takes an ad hoc verb as an argument and serializes it; the underlying self-referring system interprets the serialized representation of a verb as the corresponding verb):

Y=. ((((&>)/)((((^:_1)b.)(`(<'0';_1)))(`:6)))(&([ 128!:2 ,&<)))

Addendum: Typed Fixpoint

the Rectype Problem

In many forms of (multi-) typed - calculus (and more general type theory), a fixed-point combinator cannot be constructed, because there is no type whose terms can be applied to themselves. This is usually intentional, because it avoids the nontermination inherent in the existence of a fixed-point combinator.

• Therefore it’s impossible to construct a in STLC.

• That’s why we have to write structural recursion or prove recursion can terminate in theorem prover. e.g. the gcd fib in lean:

def gcd (a b: ℕ): ℕ :=  
  match b with         
  | 0 => a
  | b + 1 => gcd (b + 1) (a % (b + 1))
  termination_by b -- structural recursion can't be used.
  decreasing_by    -- prove that the recursion ends. i.e. a % (b + 1) < b + 1 
    simp_wf;
    apply mod_lt _ (zero_lt_of_ne_zero _);
    apply add_one_ne_zero

-- `unsafe` works as expected but can't be used in proof
unsafe def gcd_unsafe: ℕ -> ℕ -> ℕ
  | a, 0 => a
  | a, b + 1 => gcd_unsafe (b + 1) (a % (b + 1))
  
def fib(n: ℕ) :=
  match n with
  | 0 => 0
  | 1 => 1
  | k + 2 => fib (k + 1) + fib k
-- in pattern matching one must use structural recursion
-- i.e. k + 2 (= (succ (succ 2)) ) instead `k => fib (k - 1) + fib (k - 2)`
-- as it overlaps with case 0 and 1 because ∀k(k: ℕ -> k >=0).
-- though lean performs top-down matching thus the recursion does terminate,
-- it's nonterminate *definitionally*.

Fixing STLC

• Combined, we get

• However, we did not solve problem 1. As most language don’t use simply typed lambda calculus — Even if they do, it’s pretty much impossible to add a primitive.

Polymorphism

• Haskell does not allow rectypes by default even though it utilize System F. But can be broken with newtype .

• But is still ill-typed.

Rectype for Real

inductive BTree (α : Type) : Type where
  | Leaf : BTree α
  | Node : α -> BTree α -> BTree α -> BTree α

public class BTree<T> {
    T data;
    BTree<T> l, r;

    public String toString() {
        return this.l.l.l.l.l.r.r.r.r.r.r.r.data.toString();
    }
}

• Notice the use of in above expression. This means we are treating and it’s substitution (expansion) as the same type. This approach is called equirecursive.

Implementation

Mu

unsafe inductive μ (α : Type u) : Type u
  | fold : (μ α -> α) -> μ α

unsafe def unfold : μ α -> (μ α -> α)
  | .fold f => f

• let’s try unfolding it and see what happens.

unsafe def M (x : μ α) : α := unfold x x

Typed Y

unsafe def fix (t : (α -> α) -> α -> α) : α -> α :=
  let Wt : μ (α -> α) := .fold (λ f => t (unfold f f))
  M Wt

unsafe inductive μ (α : Type u) : Type u
  | fold : (μ α -> α) -> μ α

unsafe def unfold : μ α -> (μ α -> α)
  | .fold f => f

unsafe def M (x : μ α) : α := unfold x x

unsafe def fix (t : (α -> α) -> α -> α) : α -> α :=
  let Wt : μ (α -> α) := .fold (λ f => t (unfold f f))
  M Wt

unsafe def gen_factorial (f : ℕ -> ℕ) (n : ℕ) : ℕ :=
  if n = 0 then 1 else n * f (n - 1)

#eval fix gen_factorial 25 -- 15511210043330985984000000

-- recursive version
unsafe def fix_rec (f : (α -> α) -> α -> α) (x) := f (fix_rec f) x

import java.util.function.Function;

public interface YCombinator {
  interface RecursiveFunction<F> extends Function<RecursiveFunction<F>, F> { }
  public static <A,B> Function<A,B> Y(Function<Function<A,B>, Function<A,B>> f) {
    RecursiveFunction<Function<A,B>> r = w -> f.apply(x -> w.apply(w).apply(x));
    return r.apply(r);
  }

  public static void main(String... arguments) {
    Function<Integer,Integer> fac = Y(f -> n ->
      (n <= 1)
        ? 1
        : (n * f.apply(n - 1))
    );
    
    System.out.println("fac(10) = " + fac.apply(10));
  }
}

enum Mu[T] { // uppercase for type constructor
  Fold((Mu[T]) -> T)
}

fn unfold[T](folded : Mu[T]) -> (Mu[T]) -> T {
  match folded {
    Fold(f) => f
  }
}

fn m[T](x : Mu[T]) -> T { // lowercase for func name
  unfold(x)(x)
}

fn fix[T](f : ((T) -> T) -> (T) -> T) -> (T) -> T {
  let wt : Mu[(T) -> T] = Fold(fn(x) { f(fn(t : T) { unfold(x)(x)(t) }) })
  m(wt)
}

fn make_factorial(f : (Int) -> Int) -> (Int) -> Int {
  fn(n : Int) { if n == 0 { 1 } else { n * f(n - 1) } }
}

fix(make_factorial)(5) // => 120

后记