Simply Untyped Lambda Calculus的实现

学习了A Tutorial Introduction to the Lambda Calculus, by Raul Rojas这篇lecture note，简单概括了一下文章内容。

-- A Tutorial Introduction to the Lambda Calculus, by Raul Rojas 
-- https://arxiv.org/abs/1503.09060

module SU where

type Name = String
data Expr = Id Name | Lam Name Expr | App Expr Expr deriving (Eq)



instance Show Expr where
    show (Id name) = name 
    show (Lam name expr) = "(\\ " ++ name ++ " -> " ++ show expr ++ ")" 
    show (App expr1@(Lam _ _) expr2@(Lam _ _)) = "(" ++ show expr1 ++ ") (" ++ show expr2 ++ ")"
    show (App expr1@(Lam _ _) expr2@(App _ _)) = "(" ++ show expr1 ++ ") (" ++ show expr2 ++ ")"
    show (App expr1@(Lam _ _) expr2) = "(" ++ show expr1 ++ ") " ++ show expr2
    show (App expr1 expr2) = show expr1 ++ " " ++ show expr2

-- Grammar

-- 括号、左结合

-- Semantics

free :: Name -> Expr -> Bool
free n (Id name) = True
free n (Lam name expr) = n /= name && free n expr 
free n (App expr1 expr2) = free n expr1 || free n expr2

substitute :: Name -> Expr -> Expr -> Expr
substitute n e e'@(Id name) = if n == name then e else e'
substitute n e e'@(Lam name expr) = if n == name then e' else Lam name (substitute n e expr)
substitute n e (App expr1 expr2) = App (substitute n e expr1) (substitute n e expr2)

eval :: Expr -> Expr
eval (Id name) = Id name
eval (Lam name expr) = Lam name (eval expr)
eval (App (Lam name expr) e) = eval $ substitute name e expr -- beta reduction
eval (App expr1 expr2) = App (eval expr1) (eval expr2)

synonym :: Expr -> Expr -> Bool
synonym expr1 expr2 = synonym' (eval expr1) (eval expr2) where
    synonym' (Id name1) (Id name2) = name1 == name2
    synonym' (Lam name1 expr1) (Lam name2 expr2) = synonym expr1 (substitute name2 (Id name1) expr2)
    synonym' (App expr1 expr2) (App expr1' expr2') = synonym expr1 expr1' && synonym expr2 expr2'

changeName :: Name -> Name -> Expr -> Expr -- alpha conversion
changeName n n' (Id name) = Id name 
changeName n n' (Lam name expr) = if n == name 
    then Lam n' (substitute name (Id n') expr) 
    else Lam name (changeName n n' expr) 
changeName n n' (App expr1 expr2) = App (changeName n n' expr1) (changeName n n' expr2)

-- Arithmetic: Church Numeral, nat, +, *

-- Conditionals: T/F, and/or/not, conditional, pair & nat pred, nat ord

-- Recursion: Y combinator; defining recursive function by Y combinator

以及对Encoding Data in Lambda Calculus: An Introduction, by Frank (Peng) Fu的学习笔记

-- Others: 
-- Encoding Data in Lambda Calculus: An Introduction, by Frank (Peng) Fu
-- Church Encoding: better presents iteration (iterN)
-- Scott Encoding: better presents `if` (caseN, pattern matching)
-- Parigot: better presents recursion