Grassとラムダ計算とLisp

Lispのlambda式の使い方が分かってきた頃に書き溜めたラムダ計算遊び用のコードと組み合わせてみる。
まず、繰り返し関数適用してく時にCommonLispだとfuncallが大変ウザくなるので、省略するための簡単なユーティリティー関数。

(defun app (&rest arg)
  (reduce #'funcall arg))

(defun $ (&rest arg)
  (reduce #'funcall arg :from-end t))

任意の数の関数を引数にとって、appは左から、$は右から順番に適用していく。
$はHaskellにこんな感じの演算子があった様な気がしたので。
appも記号にしたかったけど良いのが思いつかなかった。

例

($ out succ out succ out succ w)

何語だコレって感じですが。スマートな書き方が分からない。
とりあえずこれをxyzzyで実行すると

xyz
#<lexical-closure: (anonymous)>

Grassに直訳

wWWWwwww
WWWw
WWWWWw
WWWWWw
WWWWWWWw
WWWWWWWw

Lisp式の左方向がスタックの上方向(Grassコードの下方向)という感じ。

チャーチ数基礎

; zero := λf x.x
(defvar zero
  (lambda (f)
    (lambda (x)
      x)))

; one := λf x.f x
(defvar one
  (lambda (f)
    (lambda (x)
      ($ f x))))

; two := λf x.f (f x)
(defvar two
  (lambda (f)
    (lambda (x)
      ($ f f x))))

0〜2をそれぞれGrassで書くと

wwv        ;0
wwWWwv     ;1
wwWWwWWWwv ;2

・使い方

(app two #'1+ 0)
; => 2

(app two out w)
; => ww

下のをGrassに直すと

wwWWwWWWwv
wWWwww
Wwwwwww

各行の意味は
1: チャーチ数の2の定義
ここからmain
2: チャーチ数の2にoutを適用
3: 2行目の結果にwを適用
結果、wが2個表示されます。

2行目でoutの代わりにsuccを適用して、そんで最後に3行目の結果をoutしてみる。

wwWWwWWWwv
wWWwwww
Wwwwwww
WWWWWw

yが1文字表示されます。

Lispで書くと

($ out (app two succ w))

チャーチ数演算

; succ := λn f x.f (n f x)
; GrassのSuccと被るので名前変更
(defvar inc
  (lambda (n)
    (lambda (f)
      (lambda (x)
        ($ f (app n f x))))))

; plus := λm n f x.m f (n f x)
(defvar plus
  (lambda (m)
    (lambda (n)
      (lambda (f)
        (lambda (x)
          (app m f (app n f x)))))))

; mult := λm n f.m (n f)
(defvar mult
  (lambda (m)
    (lambda (n)
      (lambda (f)
        ($ m n f)))))

; pow := λm n.n m
(defvar pow
  (lambda (m)
    (lambda (n)
      ($ n m))))

; tet := λm n.n (pow m) one
(defvar tet
  (lambda (m)
    (lambda (n)
      (app n ($ pow m) one))))

Grassで

;inc
wwwWWWwwWwwWWWWwv
;plus
wwwwWWWwwWwwWWWWWWwwwwWwwv
;mult
wwwWWwWWWWwv
;pow
wwWwwv

powの原理を利用して、チャーチ数の2から256を生成してみる。
で、outとwを適用。

wwWWwWWWwv
wWWww
Ww
Wwwwww
Wwwwwwwww

各行の説明
1: チャーチ数の2を定義
ここからmain
2: チャーチ数の2に自身を適用 (=2²)
3: 2行目の結果に自身を適用 (=4⁴)
4: 3行目の結果にoutを適用
5: 4行目の結果にwを適用

結果、4⁴ = 256個のwが表示されます。
Lispで書くと

(app (setf _ ($ two two)) _ out w)

最近知ったtetrationという計算もpowを利用して簡単にラムダ式で表現できたので、Grassで書いてみる。
⁴2 を計算してwの個数で結果を表示。

wwwWWWwwWwwWWWWwv
wwWWwv
wwWwwv
wwWWWwwWWwWwwwwwv
wWWWWWwwww
Ww
WWWWww
Www
Wwwwwwwwwww
Wwwwwwwwwwwwww

合わせ技なので、powとoneを先に書いておいてから定義します。
1: inc定義
2: one定義
3: pow定義
4: tetration定義
ここからmain
5: inc 1 => 2
6: 2 2 => 2² = 4
7-10: tetration 2 4 out w

実行すると大量にwを吐き出し始めますが、65536個で止まります(多分)。

一応、Lispで書くと

(app tet two ($ two two) out w)

xyzzyで実行すると丁度65536個出力されるのがルーラーで確認できます。

しんどい奴

(defvar pred
  (lambda (n)
    (lambda (f)
      (lambda (x)
        (app n
            (lambda (g)
              (lambda (h)
                ($ h g f)))
            (lambda (u) x)
            (lambda (u) u))))))

(defvar sub
  (lambda (n)
    (lambda (m)
      (app m pred n))))

めんどいのでまたいつか。
Predecessor、紙に書いて動作は確認できたけど、どうやったらこんなのが導出できるのかわからない。

例

チャーチ数 基礎

チャーチ数 演算

しんどい奴

チャーチ数基礎

チャーチ数演算