Created
August 20, 2011 11:04
-
-
Save einblicker/1158965 to your computer and use it in GitHub Desktop.
CoPL problem 76
This file contains hidden or 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
| |- let rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x) in | |
| apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) 4 | |
| evalto 49 | |
| by E-LetRec { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| (apply ((fun x -> x * x) :: (fun y -> y + 3) :: [])) 4 | |
| evalto 49 | |
| by E-App { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| apply ((fun x -> x * x) :: (fun y -> y + 3) :: []) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [])[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-AppRec { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| apply evalto ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| (fun x -> x * x) :: ((fun y -> y + 3) :: []) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] | |
| by E-Cons { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| (fun x -> x * x) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] | |
| by E-Fun {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| (fun y -> y + 3) :: [] | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] | |
| by E-Cons { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| (fun y -> y + 3) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] | |
| by E-Fun {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| [] evalto [] by E-Nil {} | |
| } | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [])[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Fun {} | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] |- | |
| 4 evalto 4 by E-Int {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4 |- | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto 49 | |
| by E-MatchCons { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4 |- | |
| l evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| f (apply l x) | |
| evalto 49 | |
| by E-App { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| f evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| ((apply l) x) | |
| evalto 7 | |
| by E-App { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| (apply l) evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [])[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-AppRec { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| apply evalto ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| l evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] )[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Fun {} | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x] :: (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun x -> x * x], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] |- | |
| x evalto 4 by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4 |- | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto 7 | |
| by E-MatchCons { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4 |- | |
| l evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| f (apply l x) | |
| evalto 7 | |
| by E-App { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| f evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| (apply l) x | |
| evalto 4 | |
| by E-App { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| apply l | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [])[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-AppRec { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| apply | |
| evalto ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| l evalto [] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [] |- | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [])[ | |
| fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)] | |
| by E-Fun {} | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3] :: [], | |
| x = 4, | |
| f = (apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)])[ | |
| fun y -> y + 3], | |
| l = [] |- | |
| x evalto 4 by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [], | |
| x = 4 |- | |
| match l with [] -> x | f :: l -> f (apply l x) | |
| evalto 4 by E-MatchNil { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [], | |
| x = 4 |- | |
| l evalto [] | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| l = [], | |
| x = 4 |- | |
| x evalto 4 by E-Var {} | |
| } | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| y = 4 |- | |
| y + 3 evalto 7 | |
| by E-Plus { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| y = 4 |- | |
| y evalto 4 by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| y = 4 |- | |
| 3 evalto 3 by E-Int {}; | |
| 4 plus 3 is 7 by B-Plus {} | |
| } | |
| } | |
| } | |
| }; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| x = 7 |- | |
| x * x evalto 49 | |
| by E-Times { | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| x = 7 |- | |
| x evalto 7 | |
| by E-Var {}; | |
| apply = ()[rec apply = fun l -> fun x -> | |
| match l with [] -> x | f :: l -> f (apply l x)], | |
| x = 7 |- | |
| x evalto 7 | |
| by E-Var {}; | |
| 7 times 7 is 49 by B-Times {} | |
| } | |
| } | |
| } | |
| } | |
| } |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment