Untype Lambda

remove names:

context is stored the information about the index of variable.
ex:
λ.x λ.y x (x y) => λ.λ.1 (1 0)

remove_name(context,x) = the index of x in the context
remove_name(context,λx.t) = λ.remove_name(x:context,t)
remove_name(context, t1 t2) = remove_name(context,t1) remove_name(context,t2)
remove_name(context, [s->k] t) = [remove_name(context,s) -> remove_name(context,k)] remove_name(context,t)

shift:

ex:
shift(2, λ.λ. 1 (0 2)) = (λ.λ. 1 (0 4))

shift(d, term) = _shift(d,0,term)

_shift(d,c,k) = if k<c then k else (k+d)
_shift(d,c, λ.t) = λ. shift(d,c+1,t)

_shift(d,c, t1 t2) = shift(d,c,t1) shift(d,c,t2)

substitution:

[s -> j] k = if s==k then j else k
[s -> j] λ.t = λ. [s+1 -> shift(1,j)] t
[s -> j] t1 t2 = [s->j] t1 [s->j] t2

evaluation:

ex:
(λ.1 0 2) (λ.0) → 0 (λ.0) 1 (not 1 (λ.0) 2).

(λ. t1) t2 = shift(-1,[0 -> shift(1,t2)] t1)

BNF-converter grammar:

entrypoints Program;
Prog.           Program::=[Def];separator Def ";" ;
TermDef.        Def::= Term;

AbsTerm.        Term::= "lambda" Ident "." Term;

AppTerm.        Term1::=Term1 Term2;

IdTerm.         Term2::= Ident;

coercions Term 2;

Haskell code:
import Control.Monad
import System.Environment (getArgs)
import System.Exit (exitFailure)
import Abssyntax
import Lexsyntax
import Parsyntax
import ErrM

data TermNameless = Var Int | Abs TermNameless | App TermNameless TermNameless
data NameBind = MkNameBind
type Context = [(String,NameBind)]

find_index :: Context -> String -> Int -> Int
find_index ((x,_):q) y i = if x == y then i else find_index q y (i+1)

_remove_name :: Context -> Term -> TermNameless
_remove_name ctx (AbsTerm (Ident x) term) = Abs (_remove_name ((x,MkNameBind):ctx) term)
_remove_name ctx (AppTerm t1 t2) = App (_remove_name ctx t1) (_remove_name ctx t2)
_remove_name ctx (IdTerm (Ident x)) = Var (find_index ctx x 0)

-- change the parse result into nameless lambda calcus
remove_name :: Def -> TermNameless
remove_name (TermDef def) = _remove_name [] def

printTermNameless :: TermNameless -> IO ()
printTermNameless (Var x) = do putStr (" "++show x++" ")
printTermNameless (Abs t) = do putStr "(lambda . "
                               printTermNameless t
                               putStr ")"
printTermNameless (App t1 t2) = do printTermNameless t1
                                   printTermNameless t2
_shift::Int -> Int -> TermNameless -> TermNameless
_shift c d (Var x) = if x < c then (Var x) else (Var (x+d))
_shift c d (Abs t) = (Abs (_shift (c+1) d t))
_shift c d (App t1 t2) = (App (_shift c d t1) (_shift c d t2))

shift :: Int -> TermNameless -> TermNameless
shift d t = _shift 0 d t

substitute:: TermNameless -> TermNameless -> TermNameless -> TermNameless
substitute (Var s) k (Var x) = if x == s then k else (Var x)
substitute (Var s) k (Abs t) = (Abs (substitute (Var (s+1)) (shift 1 k) t))
substitute s k (App t1 t2) = (App (substitute s k t1) (substitute s k t2))

eval::TermNameless -> TermNameless
eval (App (Abs t) t1) = shift (-1) (substitute (Var 0) (shift 1 t1) t)
eval (App t1 t2) = (App (eval t1) (eval t2))
eval x = x

out :: TermNameless -> IO ()
out t = do printTermNameless t
           putStrLn "\n"

check :: String -> IO ()
check s = case pProgram (myLexer s) of
            Bad err  -> do putStrLn "SYNTAX ERROR"
                           putStrLn err
                           exitFailure
            Ok  (Prog tree) -> do sequence_ $ map out result
                                  --putStrLn $ show tree
                                  where
                                  result = map (eval.remove_name) tree
main :: IO ()
main = do args <- getArgs
          case args of
            [file] -> readFile file >>= check
            _ -> do putStrLn "Usage: lambda <sourceFile>"
                    exitFailure
pl
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License