λ式の Combinatory Logic変換とその評価

λ式の構文ルール

E = \x.E | E1 E2 | V | C
V = 変数
C = 定数

Combinator Logic(CL)はS K Iコンビネータ。CLで計算を表現すると、束縛変数がなくなるのがいいところ。

λ式をCLに変換するルール

[]\x.E => [x]E
[](E1 E2) => []E1 []E2
[]v => v

[x]\y.E => [x]([y]E)
[x](E1 E2) => S [x]E1 [x]E2
[x]x => I
[x]v => K v
  : v = S, K, I, consts, freevars

CL評価ルール

[[S x y z]] => [[x z (y z)]]
[[K x y]] => [[y]]
[[I x]] => [[x]]
[[a b]] => [[[[a]] [[b]]]]
[[c]] => c
  : c = consts

λ式=>CL変換例

\x.\y.y x =>
[x](\y.y x) =>
[x]([y](y x)) =>
[x](S [y]y [y]x) =>
[x](S I (K x)) =>
[x](S I (K x)) =>
S [x](S I) [x](K x) =>
S (S [x]S [x]I) (S [x]K [x]x) =>
S (S (K S) (K I)) (S (K K) I)

CL評価例

[(\x.\y.y x) z s ==> s z]

S (S (K S) (K I)) (S (K K) I) z s =>
(S (K S) (K I)) z (S (K K) I z) s =>
(K S) z (K I z) (S (K K) I z) s =>
S (K I z) (S (K K) I z) s =>
(K I z) s (S (K K) I z s) =>
I s (S (K K) I z s) =>
s (S (K K) I z s) =>
s ((K K) z (I z) s) =>
s (K (I z) s) =>
s (I z) =>
s z

Haskellコード

data Term = Lam String Term | App Term Term | Var String | Con String
  deriving Show
data Comb = Comb `P` Comb | S | K | I | V String | C String
  deriving (Show, Eq)

toCL (Lam n body) = trans n body
toCL (App opr opd) = (toCL opr) `P` (toCL opd)
toCL (Var x) = (V x)
toCL (Con v) = (C v)

trans p (Lam n body) = trans2 p (trans n body)
trans p (App opr opd) = S `P` (trans p opr) `P` (trans p opd)
trans p (Var x) | p == x = I
trans p (Var x) = K `P` (V x)
trans p (Con v) = K `P` (C v)

trans2 p (a `P` b) = S `P` (trans2 p a) `P` (trans2 p b)
trans2 p (V x) | p == x = I
trans2 p a = K `P` a

eval (S `P` x `P` y `P` z) = eval (x `P` z `P` (y `P` z))
eval (K `P` x `P` y) = eval x
eval (I `P` x) = eval x
eval (a `P` b) = let na = eval a in
                 let nb = eval b in
                 if a /= na || b /= nb then eval (na `P` nb) else (a `P` b)
eval a = a

-- toCL (Lam "x" (Lam "y" (App (Var "y") (Var "x"))))
-- eval ((toCL (Lam "x" (Lam "y" (App (Var "y") (Var "x"))))) `P` (C "zero") `P` (C "succ"))

実行例

$ ghci combinatory.hs
GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main             ( combinatory.hs, interpreted )
Ok, modules loaded: Main.
*Main> toCL (Lam "x" (Lam "y" (App (Var "y") (Var "x"))))
(S `P` ((S `P` (K `P` S)) `P` (K `P` I))) `P` ((S `P` (K `P` K)) `P` I)
*Main> eval ((toCL (Lam "x" (Lam "y" (App (Var "y") (Var "x"))))) `P` (C "zero") `P` (C "succ"))
C "succ" `P` C "zero"
*Main>