Last active
November 5, 2019 09:45
-
-
Save fedelebron/57d89e44a05184c99c01b69767468055 to your computer and use it in GitHub Desktop.
Short demo of a lambda calculus curiosity, from Mirai Ikebuchi, Keisuke Nakano "On repetitive right application of B-terms" 2018
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE OverloadedStrings #-} | |
import qualified Data.Set as S | |
import Data.String | |
import Data.List | |
type Var = String | |
data Expr = V Var | Ap Expr Expr | Lambda Var Expr | |
deriving Eq | |
instance IsString Expr where | |
fromString = V | |
λ = Lambda | |
instance Show Expr where | |
show (V x) = x | |
show (Ap f x) = '(' : show f ++ show x ++ ")" | |
show (Lambda v e) = case show e of | |
'(':'λ':s -> "(λ" ++ v ++ s | |
r -> "(λ" ++ v ++ "." ++ r ++ ")" | |
free :: Expr -> S.Set Var | |
free (V x) = S.singleton x | |
free (Lambda v e) = free e `S.difference` S.singleton v | |
free (Ap f e) = free f `S.union` free e | |
alpha :: Var -> Var -> Expr -> Expr | |
alpha x = subst x . V | |
subst :: Var -> Expr -> Expr -> Expr | |
subst v e' = go | |
where | |
go (V v') | v == v' = e' | |
| otherwise = V v' | |
go (Ap f e) = Ap (go f) (go e) | |
go (Lambda x e) | x == v = Lambda x e | |
| x `notElem` free e' = Lambda x (go e) | |
| otherwise = let y = fresh (Ap e e') | |
in Lambda y (go (alpha x y e)) | |
usedVars :: Expr -> [Var] | |
usedVars (V x) = [x] | |
usedVars (Ap f e) = usedVars f ++ usedVars e | |
usedVars (Lambda y e) = y:usedVars e | |
allVars :: [Var] | |
allVars = (map return "fghabcdevw") ++ ["v_" ++ show i | i <- [0..]] | |
fresh :: Expr -> Var | |
fresh = head . (allVars \\) . usedVars | |
normal :: Expr -> Bool | |
normal (V x) = True | |
normal (Ap Lambda{} _) = False | |
normal (Ap f x) = normal f && normal x | |
normal (Lambda x e) = normal e | |
beta :: Expr -> Expr | |
beta (V x) = V x | |
beta (Lambda x e) = Lambda x (beta e) | |
beta (Ap (Lambda x e) e') = subst x e' e | |
beta (Ap (V r) e) = Ap (V r) (beta e) | |
beta (Ap f e) = if normal f then Ap f (beta e) | |
else Ap (beta f) e | |
beta' :: Expr -> Expr | |
beta' = until normal beta | |
-- This assumes terms are both beta and eta normalized. | |
alphaEq :: Expr -> Expr -> Bool | |
alphaEq (V x) (V y) = x == y | |
alphaEq (Lambda x e) (Lambda y f) = alpha y x f `alphaEq` e | |
alphaEq (Ap f e) (Ap g e') = f `alphaEq` g && e `alphaEq` e' | |
alphaEq _ _ = False | |
lid = λ"x" "x" | |
ldot = λ"g" (λ"f" (λ"x" (Ap "g" (Ap "f" "x")))) | |
lflip = λ"f" (λ"x" (λ"y" (Ap (Ap "f" "y") "x"))) | |
power 1 x = x | |
power n x = power (n - 1) x `Ap` x | |
test e n m = do | |
let left = beta' (power n e) | |
right = beta' (power m e) | |
putStrLn (show e ++ "^" ++ show n ++ " = " ++ show left) | |
putStrLn (show e ++ "^" ++ show m ++ " = " ++ show right) | |
print (left `alphaEq` right) | |
main = do | |
test lid 1 2 | |
test lflip 3 4 | |
-- Note ldot is fmap for the Hom(a, _) functor. | |
test ldot 6 10 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment