ラムダ計算

前に作ったもの。ラムダ計算のベータ簡約をHaskellで実装。

module Lambda where
import Data.List
type Val = String
data Lambda = V Val | A Lambda Lambda | L Val Lambda
instance Show Lambda where
show (V x) = x
show (A m n) = show' m ++ show'' n
where
show' (V x) = x
show' m@(A _ _) = show m
show' m@(L _ _) = "("++ show m ++")"
show'' (V x) = x
show'' m@(A _ _) = "("++ show m ++")"
show'' m@(L _ _) = "("++ show m ++")"
show (L x m) = ""++ x ++ "."++ show m
-- 変数
vals ::[Val]
vals = words "a b c d e f g h i j k l m n o p q r s u v w x y z"
-- 代入
subst :: Lambda -> Val -> Lambda -> Lambda
subst (V y) x n = if y==x then n else (V y)
subst (A m1 m2) x n = subst m1 x n `A` subst m2 x n
subst (L y m) x n = if y/=x && notElem y fn
then L y $ subst m x n
else if null . () vals $ fn++[y]++freeV m
then (V "too many variables")
else subst (L z $ subst m y $ V z ) x n
where fn = freeV n
z = last . () vals $ fn++[y]++freeV m
-- 自由変数
freeV :: Lambda -> [Val]
freeV (V x) = [x]
freeV (A m n) = freeV m `union` freeV n
freeV (L x m) = freeV m  [x]
-- β-簡約
beta :: Lambda -> Lambda
beta (V x) = V x
beta (L x m) = L x $ beta m
beta ((L x m) `A` n) = beta $ subst m x n
beta ((V x) `A` m) = V x `A` beta m
beta (m `A` n) = beta $ value m `A` n
-- Value = V Val `A` Lambda | L Val `A` Lambda
value :: Lambda -> Lambda
value (V x) = V x
value (L x m) = L x m
value ((L x m) `A` n) = value $ subst m x n
value ((V x) `A` m) =V x `A` value m
value (m `A` n) = value $ value m `A` n
-- one time (?) paralle beta-reduction
pbeta :: Lambda -> Lambda
pbeta (V x) = V x
pbeta (L x m) = L x $ pbeta m
pbeta ((L x m) `A` n) = subst m x n
pbeta (m `A` n) = pbeta m `A` pbeta n
-- n times(?) paralle beta-reduction
pbeta' n = foldl1 (.) . (take n ) . repeat $ pbeta
-- よく使う変数
u = V "u"
v = V "v"
w = V "w"
x = V "x"
y = V "y"
z = V "z"
-- Combinator
i = L "x" x
k = L "x" $ L "y"  x
s = L "x" $ L "y" $ L "z" $ x`A`z`A`(y`A`z)
b = L "x" $ L "y" $ L "z" $ x`A`(y`A`z)
c = L "x" $ L "y" $ L "z" $ x`A`z`A`y
q = L "y" $ lam `A` lam
where lam = L "x" $ y `A` ( x`A`x)
m = L "x" $ x `A` x
o  =m `A` m
-- 不動点演算子 theta
theta = th `A` th
th = L "x" $ L "y" $ y `A` ( x `A` x `A` y)
-- Church numeral 
zero = L "z" $ L "y" z
--zero = L"z" $ L "y" y
one = beta $ suc `A` zero
two = beta $ suc `A` one
three = beta $ suc `A` two
four = beta $ suc `A` three
five = beta $ suc `A` four
six = beta $ suc `A` five
seven = beta $ suc `A` six
eight = beta $ suc `A` seven
nine = beta $ suc `A` eight
-- 算術演算子
suc = L "x" $ L "y" $ L "z" $ z `A` (x`A`y`A`z)
--suc = L "x" $ L"y" $ L "z" $ y `A` (x `A` y `A` z)
add  =L "x" $ L "y" $ y `A` x `A` suc
mult =L "x" $ L "y" $ y `A` zero `A` (add `A` x)
pre = L "x" $ L "y" $ L "z"$ x `A`(L"u" y)`A`t`A`(L"u" $ u)
where t = L "g" $ L "h" $ V"h" `A` (V"g" `A` z)
sub = L "x" $ L "y" $ y `A` x `A` pre
-- bool
true = L "x" $ L "y" x
false = L "x" $ L "y" y
if' = L "x" $ L "y" $ L "z" $ x`A`y`A`z
isZero = L "x" $ x `A` true `A` (L "y" false)
leq = L "x" $ L "y" $ isZero `A` (sub `A` x `A` y)
and' = L "x" $ L "y" $ if' `A` x `A` y `A` false
or' =  L "x" $ L "y" $ if' `A` x `A` true `A` y
neg = L"x" $ if' `A` x `A` false `A` true
eq = L "x" $ L "y" $ and' `A` (leq `A` x `A` y) `A` (leq `A` y `A` x)
even' = rec `A` neg `A` true
-- tuple 
pair = L "x" $ L "y" $ L"z" $ z `A` x `A` y
first = L "x" $ x `A` true
second = L "x" $ x `A` false
-- recursion
-- f(0) = a
-- f(n+1) = g(f(n))
rec = L"g" $ L "a" $ L "x" $ x `A` V "a" `A` V "g"
-- recursion2
-- f(0) = a
-- f(n+1) = g(f(n),n)
rec2 = L "g" $ L "a" $ L "x" $ first `A` (rec `A` g' `A` a' `A` x)
where g' = L "x" $ pair `A` (V "g" `A` (first `A` x) `A` (second `A` x)) `A` (suc `A` (second `A` x))
a' = pair `A` V "a" `A` zero
-- halfCeil n は n/2以上の最小整数を返す
halfCeil = rec2 `A` g `A` zero
where g = L "x" $ L"y" $ if' `A` (even' `A` y) `A` (suc `A` x) `A` x
-- 割ったあまり
rem' = q `A` (L "z" $ L "x" $ L "y" g)
where g = if' `A` (leq `A` y `A` x) `A` (z `A` (sub `A` x `A` y) `A`y) `A` x
-- 階乗
fact = L "x" $ (q `A` f) `A` x
where f = L "fct" $ L "x" $ if' `A` (isZero `A` x) `A` one `A` (mult `A` x `A` (V "fct" `A` (pre `A` x)))
-- 素数判定
isPrime = L "x" $ if' `A` (eq `A` x `A` two) `A` true `A` f
where f = if' `A` (eq `A` x `A` four) `A` false `A` ((q `A` g) `A` two)
g = L "z" $ L "y" $ if' `A` (eq `A` y `A` (halfCeil `A` x)) `A` true `A` h
h = if' `A` (isZero `A` (rem' `A` x`A` y)) `A` false `A` (z`A` (suc `A` y))
-- Ackermann
-- http://en.wikipedia.org/wiki/Ackermann_function
ack = L "m" $ rec `A` iter `A` suc `A` V "m"
where iter = L "f" $ rec `A` V "f" `A` (V "f" `A` one)
-- Church numberからIntへの変換
churchToInt :: Lambda -> Int
churchToInt (L f (L x m)) = g m
where g (V x) = 
g (V f `A` n) = 1 + (g n)
-- IntからChurch numberへの変換
intToChurch :: Int -> Lambda
intToChurch  = zero
intToChurch (n+1) =beta $  suc `A` (intToChurch n)
-- ラムダ項からBoolへの変換
lambdaToBool :: Lambda -> Bool
lambdaToBool (L t (L f (V b))) = if t == b then True else False