We now want to consider a functional programming langage with the following syntax (expressions are denoted by variables "e") variables are denoted by "x", "y" or "f", "g" patterns are denoted by variables "p": expressions: let x = e1 in e let rec x = e1 in e2 e1 < e2 x n e1 + e2, e1 * e2, e1 - e2, Nil Cons e1 e2 true false match e with p1 -> e1 | p2 -> e2 fun x -> e e1 e2 patterns: x Cons p1 p2 Nil true false Abbreviation: if e then e1 else e2 == match e with true -> e1 | false -> e2 Examples (all executed in empty context) let x = 1 + 3 in x + x --> 8 let x = Cons 1 Nil in match x with Nil -> 0 | Cons x1 y1 -> 1 --> 1 let x = Cons 1 Nil in match x with Nil -> 0 | Cons x1 y1 -> y1 --> Nil let x = 3 in let f = fun y -> x + y in let x = 4 in f 2 --> 5 let rec f = fun x -> if x < 1 then 1 else x*(f(x-1)) in f 3 --> 6 let rec g = fun x -> fun y -> match x with Nil -> y | Cons x1 x2 -> Cons x1 (g x2 y) in g (Cons 1 Nil) (Cons 2 Nil) --> Cons 1 (Cons 2 Nil) Semantic rules: Gamma |- x -> v x<>y --------------- --------------------- ---------------------- Gamma |- n -> n (x,v).Gamma |- x -> v (y,v').Gamma |- x -> v true, false, <, +, *, -, Nil is like true and false. Gamma |- e1 -> v1 Gamma |- e2 -> v2 ------------------------------------ Gamma |- Cons e1 e2 -> Cons v1 v2 ---------------------------- Gamma |- v, x -> (x,v).Gamma Gamma |- v1, p1 -> Gamma' Gamma' |- v2, p2 -> Gamma'' ------------------------------------------------------ Gamma |- Cons v1 v2, Cons p1 p2 -> Gamma'' ---------------------------- ------------------------------ Gamma |- true, true -> Gamma Gamma |- false, false -> Gamma ---------------------- -------------------------- Gamma |- n, n -> Gamma Gamma |- Nil, Nil -> Gamma Gamma |- e -> v Gamma |- v,p1 -> Gamma' Gamma' |- e1 -> v1 ------------------------------------------------------------ Gamma |- match e with p1 -> e1 | ... -> v1 Gamma |- e -> v (forall Gamma', not (Gamma |- v,p1 -> Gamma')) Gamma |- match e with p2 -> e2 .... -> v1 --------------------------------------------------------------- Gamma |- match e with p1 -> e1 | p2 -> e2 .... -> v1 --------------------------------------------- Gamma |- (fun x -> e) -> e, Gamma> Gamma |- e1 -> e, Gamma'> Gamma |- e2 -> v2 (x,v2).Gamma' |- e -> v ------------------------------------------------------ Gamma |- e1 e2 -> v Gamma |- e1 -> v1 (x,v1).Gamma |- e2 -> v2 ---------------------------------------------- Gamma |- let x = e1 in e2 -> v2 Gamma |- e1 -> v1 (x, rec(x,v1)).Gamma |- e2 -> v2 ----------------------------------------------------- Gamma |- let rec x = e1 in e2 -> v2 Gamma |- e1 -> rec(y, e, Gamma'>) Gamma |- e2 -> v2 (x,v2).(y ,rec(y, e, Gamma'>)).Gamma' |- e -> v ----------------------------------------------------------- Gamma |- e1 e2 -> v EXAMPLE derivations: ==================== E1 == let rec f = fun x -> if x < 1 then 0 else x+(f(x-1)) in f 2 E2 == fun x -> if x < 1 then 0 else x+(f(x-1)) E3 == f 2 E4 == if x < 1 then 0 else x+(f(x-1)) V2 == E4, empty> C1 == (f,rec(f,V2)).empty C2 == (x,2).(f,rec(f,V2)).empty E5 == x+(f(x-1)) V5 == 2+V6 V5 == V3 C3 == (x,1).C1 V6 == 1+ V7 C4 == (x,0).C1 V7 == 0 (V6 = 1, V5 = 3) ----------------------------------- empty |- E2 -> E4, empty> (admis) ---------------------- ------------ C4 |- x < 1 -> true C4 |- true, true -> C4 C4 |- 0 -> 0 d5 ------------------------------------------------------------ (x,0).C1 |- if x < 1 then .... -> 0 d5 ======= . ....... (x,0).C1 |- E4 -> V7 d4 -------------------------------------- (x,1).C1 |- E4 -> V6 d4 ==================== =============== . C2 |- f -> rec(f,V2) C2 |- x -1 -> 1 (x,1).C1 |- E4 -> V6 ------------ ------------------------------------------------------------------ C2 |- x -> 2 C2 |- f (x-1) -> V6 -------------------------- d3 C2 |- x + f (x - 1) --> V5 d3 . (admis) ------------------------ . C2 |- x < 1 -> false C2 |- false, false -> C2 C2 |- E5 -> V5 ----------------------------------------------------------------- d''= C2 |- match x < 1 with false -> E5 -> V5 (ADMIS) (ADMIS) C2 |- x < 1 -> false (forall Gamma, not(C2 |- false,true -> Gamma)) ... d'' C2 |- match x < 1 with false -> E5 -> V5 d'= ------------------------------------------------------------------------ C2 |- match x < 1 with true -> 0 | false -> x+(f(x-1)) -> V5 d' . -------------------- ------------ . C1 |- f -> rec(f,V2) C1 |- 2 -> 2 (x,2).(f,rec(f,V2)).empty |- E4 -> V5 d= ------------------------------------------------------------------------------- C1 |- f 2 -> V5 d . ----------------- . empty |- E2 -> V2 (f,rec(f,V2)).empty |- E3 -> V3 ------------------------------------------------------------------------ empty |- E1 -> V3