== Typed Lambda Calculus ==
Replace the data type exp in /interpreter/interpreter.ml
with the following data type:
type exp =
| True
| False
| If of exp * exp * exp
| Num of int
| IsZero of exp
| Plus of exp * exp
| Mult of exp * exp
| Var of string
| Lambda of string * typ * exp
| Apply of exp * exp
Add the following exception
exception Substitution_error
Create the function: free_variables : exp -> string list
let rec free_variables (e : exp) = … insert code …
(free_variables e) returns a list of strings, which are the names of the variables that are free in e. free_variables must be implemented according to the function definition
that we have seen in class.
Create the function: substitution : exp -> string -> exp -> exp
let rec substitution (e1 : exp) (x : string) (e2 : exp) = … insert code …
(substitution e1 “x” e2) replaces all the free occurrences of “x” in the expression e1 with e2, according to the substitution algorithm that we have seen in class.
The function substitution raises the exception Substitution_error for the case of variable capture that we have seen in class.
Modify the function step to add the behavior for Apply.
Replace the data type typ with
type typ =
| TBool
| TInt
| TArrow of typ * typ
Add the following data type
type type_environment = (string * typ) list
Modify the function type_check to be: type_check :
let rec type_check (te : type_environment) (e : exp) = … modify your previous code …
… add the cases for variables, functions, and applications …
Test the functions
– substitution
– multi_step
– type_check
with the following inputs:
1) substitute x with 2 in
(5 + x) * (3 + x) = (5 + 2) * (3 + 2)
(substitution
(Mult (Plus (Num 5, Var “x”), Plus (Num 3, Var “x”)))
“x” (Num 2))
Output: (Mult (Plus (Num 5, Num 2), Plus (Num 3, Num 2)))
2) substitute y with (5 * x) in
if (isZero y) then y else x = if (isZero (5 * x)) then (5 * x) else x
(substitution
(If (IsZero (Var “y”), Var “y”, Var “x”))
“y”
(Mult (Num 5, Var “x”)))
Output: (If (IsZero (Mult (Num 5, Var “x”)), Mult (Num 5, Var “x”), Var “x”))
3) substitute x with 0 in
(lambda x:int.(x + 5)) = (lambda x:int.(x + 5))
(substitution (Lambda (“x”, TInt, Plus (Var “x”, Num 5))) “x” (Num 0))
Output: (Lambda (“x”, TInt, Plus (Var “x”, Num 5)))
4) substitute y with (lambda x:int.(x + 1)) in
(lambda x:bool.if x then (y 0) else (y 1)) = (lambda x:bool.if x then ((lambda x:int.(x + 1)) 0) else ((lambda x:int.(x + 1)) 1))
(substitution
(Lambda
( “x”
, TBool
, If (Var “x”, Apply (Var “y”, Num 0), Apply (Var “y”, Num 1)) ))
“y”
(Lambda (“x”, TInt, Plus (Var “x”, Num 1))))
Output:
(Lambda ( “x”
, TBool , If
( Var “x”
, Apply (Lambda (“x”, TInt, Plus (Var “x”, Num 1)), Num 0)
, Apply (Lambda (“x”, TInt, Plus (Var “x”, Num 1)), Num 1) ) ))
5) ((lambda x:int.((5 + x) * (3 + x))) 2) => 35
(multi_step
(Apply
( Lambda
(“x”, TInt, Mult (Plus (Num 5, Var “x”), Plus (Num 3, Var “x”)))
, Num 2 )))
Output: (Num 35)
6) (lambda x:int.(x + 5)) => (lambda x:int.(x + 5))
(multi_step (Lambda (“x”, TInt, Plus (Var “x”, Num 5))))
Output: (Lambda (“x”, TInt, Plus (Var “x”, Num 5)))
7) (((lambda y:(int -> int).(lambda x:bool.if x then (y 0) else (y 1))) (lambda x:int.(x + 1))) false) => 2
(multi_step
(Apply
( Apply
( Lambda
( “y”
, TArrow (TInt, TInt)
, Lambda
( “x”
, TBool
, If
( Var “x”
, Apply (Var “y”, Num 0)
, Apply (Var “y”, Num 1) ) ) )
, Lambda (“x”, TInt, Plus (Var “x”, Num 1)) )
, False )))
Output: (Num 2)
8) ((lambda x:bool.if x then 7 else 33) ((lambda x:int.(isZero x)) 5)) => 33
(multi_step
(Apply
( Lambda (“x”, TBool, If (Var “x”, Num 7, Num 33))
, Apply (Lambda (“x”, TInt, IsZero (Var “x”)), Num 5) )))
Output: (Num 33)
9) ((lambda x:int.(x + y)) 0) => Eval_error
(multi_step (Apply (Lambda (“x”, TInt, Plus (Var “x”, Var “y”)), Num 0)))
Output: Eval_error
10) (((((lambda x.int.(lambda x:int.(lambda z:int.((x + x) * z))))) 1) 2) 3) => 12
(multi_step
(Apply
( Apply
( Apply
( Lambda ( “x”
, TInt
, Lambda
( “x”
, TInt
, Lambda
)
, Num 1 )
, Num 2 )
, Num 3 )))
( “z”
, TInt
, Mult (Plus (Var “x”, Var “x”), Var “z”) ) )
Output: (Num 12)
11) ((lambda x:(int -> (int -> (int -> int))).(((x 7) 6) 8)) (lambda x:int.(lambda y:int.(lambda z:int.((x * y) + z))))) => 50
(multi_step
(Apply
( Lambda ( “x”
, TArrow (TInt, TArrow (TInt, TInt))
, Apply (Apply (Apply (Var “x”, Num 7), Num 6), Num 8) )
, Lambda
( “x”
, TInt
, Lambda
( “y”
, TInt
, Lambda
(“z”, TInt, Plus (Mult (Var “x”, Var “y”), Var “z”)) )
) )))
Output: (Num 50)
12) ((5 + 2) (lambda x:int.x)) => Eval_error
(multi_step (Apply (Plus (Num 5, Num 2), Lambda (“x”, TInt, Var “x”))))
Output: Eval_error
13) ((lambda x:int.((5 + x) * (3 + x))) 2) is of type int
(type_check []
(Apply
( Lambda
(“x”, TInt, Mult (Plus (Num 5, Var “x”), Plus (Num 3, Var “x”)))
, Num 2 )))
Outout: TInt
14) (lambda x:int.(x + 5)) is of type (int -> int)
(type_check [] (Lambda (“x”, TInt, Plus (Var “x”, Num 5))))
Output: (TArrow (TInt, TInt))
15) (((lambda y:(int -> int).(lambda x:bool.if x then (y 0) else (y 1))) (lambda x:int.(x + 1))) false) is of type int
(type_check []
(Apply
( Apply
( Lambda
( “y”
, TArrow (TInt, TInt)
, Lambda
( “x”
, TBool
, If
( Var “x”
, Apply (Var “y”, Num 0)
, Apply (Var “y”, Num 1) ) ) )
, Lambda (“x”, TInt, Plus (Var “x”, Num 1)) )
, False )))
Output: TInt
16) ((lambda x:bool.if x then 7 else 33) ((lambda x:int.(isZero x)) 5)) is of type int
(type_check []
(Apply
( Lambda (“x”, TBool, If (Var “x”, Num 7, Num 33))
, Apply (Lambda (“x”, TInt, IsZero (Var “x”)), Num 5) )))
Output: TInt
17) ((lambda x:int.(x + y)) 0) is a Type_error
(type_check []
(Apply (Lambda (“x”, TInt, Plus (Var “x”, Var “y”)), Num 0)))
Output: Type_error
18) (((((lambda x.int.(lambda x:int.(lambda z:int.((x + x) * z))))) 1) 2) (lambda x:int.x)) is a Type_error
(type_check []
(Apply
( Apply
( Apply
( Lambda ( “x”
, TInt
, Lambda
( “x”
, TInt
, Lambda
( “z”
, TInt
, Mult (Plus (Var “x”, Var “x”), Var “z”) ) )
)
, Num 1 )
, Num 2 )
, Lambda (“x”, TInt, Var “x”) )))
Output: Type_error
19) (lambda x:(int -> (int -> (int -> int))).(((x 7) 6)) (lambda x:int.(lambda y:int.(lambda z:int.((x * y) + z))))) is of type (int -> int)
(type_check []
(Apply
( Lambda ( “x”
, TArrow (TInt, TArrow (TInt, TArrow (TInt, TInt)))
, Apply (Apply (Var “x”, Num 7), Num 6) )
, Lambda
( “x”
, TInt
, Lambda
( “y”
, TInt
, Lambda
(“z”, TInt, Plus (Mult (Var “x”, Var “y”), Var “z”)) )
) )))
Output: TArrow (TInt, TInt)
20) ((5 + 2) (lambda x:int.x)) is a Type_error
(type_check []
(Apply (Plus (Num 5, Num 2), Lambda (“x”, TInt, Var “x”))))
Output: Type_error
IMPORTANT: TESTS ARE NUMBERED AND MUST BE PASSED SEQUENTIALLY TO OBTAIN THE SCORE BELOW.
Score:
Succeding tests 1-4 = 0.73
Succeding tests 5-12 = 0.74
Succeding tests 13-20 = 0.75