From 5ab9d6a956e6750c6aa46f97b724bffbb01a8d0f Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Mon, 25 Oct 2010 15:06:51 -0400 Subject: [PATCH] edits --- assignment5.mdwn | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/assignment5.mdwn b/assignment5.mdwn index bd89880e..72361897 100644 --- a/assignment5.mdwn +++ b/assignment5.mdwn @@ -142,10 +142,12 @@ Baby monads match x with None -> None | Some n -> f n;; -Booleans, Church numbers, and Church lists in System F ------------------------------------------------------- +Booleans, Church numbers, and Church lists in OCAML +--------------------------------------------------- These questions adapted from web materials written by some smart dude named Acar. +The idea is to get booleans, Church numbers, "Church" lists, and +binary trees working in OCAML. Recall from class System F, or the polymorphic Î»-calculus. @@ -157,11 +159,10 @@ These questions adapted from web materials written by some smart dude named Acar boolÂ :=Â âÎ±.Â Î±Â âÂ Î±Â âÂ Î± trueÂ :=Â ÎÎ±.Â Î»t:Î±.Â Î»fÂ :Î±.Â t falseÂ :=Â ÎÎ±.Â Î»t:Î±.Â Î»fÂ :Î±.Â f - ifÏÂ eÂ thenÂ e1Â elseÂ e2Â :=Â eÂ [ÏÂ ]Â e1Â e2 (whereÂ ÏÂ indicatesÂ theÂ typeÂ ofÂ e1Â andÂ e2) - ExerciseÂ 1.Â ShowÂ howÂ toÂ encodeÂ theÂ followingÂ terms.Â NoteÂ thatÂ eachÂ ofÂ theseÂ terms,Â whenÂ appliedÂ toÂ the + NoteÂ thatÂ eachÂ ofÂ the followingÂ terms,Â whenÂ appliedÂ toÂ the appropriateÂ arguments,Â returnÂ aÂ resultÂ ofÂ typeÂ bool. (a)Â theÂ termÂ notÂ thatÂ takesÂ anÂ argumentÂ ofÂ typeÂ boolÂ andÂ computesÂ itsÂ negation; @@ -178,8 +179,8 @@ These questions adapted from web materials written by some smart dude named Acar encodingÂ above,Â theÂ resultÂ ofÂ thatÂ iterationÂ canÂ beÂ anyÂ typeÂ Î±,Â asÂ longÂ asÂ youÂ haveÂ aÂ baseÂ elementÂ zÂ :Â Î±Â and aÂ functionÂ sÂ :Â Î±Â âÂ Î±. - ExerciseÂ 2.Â VerifyÂ thatÂ theseÂ encodingsÂ (zero,Â succÂ ,Â rec)Â typecheckÂ inÂ SystemÂ F. - (Draw a type tree for each term.) + **Excercise**: get booleans and Church numbers working in OCAML, + including OCAML versions of bool, true, false, zero, succ, add. ConsiderÂ theÂ followingÂ listÂ type: @@ -189,24 +190,25 @@ These questions adapted from web materials written by some smart dude named Acar ÏÂ listÂ :=Â âÎ±.Â Î±Â âÂ (ÏÂ âÂ Î±Â âÂ Î±)Â âÂ Î± nilÏÂ :=Â ÎÎ±.Â Î»n:Î±.Â Î»c:ÏÂ âÂ Î±Â âÂ Î±.Â n - consÏÂ :=Â Î»h:Ï.Â Î»t:ÏÂ list.Â ÎÎ±.Â Î»n:Î±.Â Î»c:ÏÂ âÂ Î±Â âÂ Î±.Â cÂ hÂ (tÂ [Î±]Â nÂ c) + makeListÏÂ :=Â Î»h:Ï.Â Î»t:ÏÂ list.Â ÎÎ±.Â Î»n:Î±.Â Î»c:ÏÂ âÂ Î±Â âÂ Î±.Â cÂ hÂ (tÂ [Î±]Â nÂ c) - AsÂ withÂ nats,Â TheÂ ÏÂ listÂ typeâsÂ caseÂ analyzingÂ eliminationÂ formÂ isÂ justÂ application. + AsÂ withÂ nats,Â recursion is built into the datatype. WeÂ canÂ writeÂ functions likeÂ map: mapÂ :Â (ÏÂ âÂ ÏÂ )Â âÂ ÏÂ listÂ âÂ ÏÂ list :=Â Î»fÂ :ÏÂ âÂ Ï.Â Î»l:ÏÂ list.Â lÂ [ÏÂ list]Â nilÏÂ (Î»x:Ï.Â Î»y:ÏÂ list.Â consÏÂ (fÂ x)Â y - ExerciseÂ 3.Â ConsiderÂ theÂ followingÂ simpleÂ binaryÂ treeÂ type: + **Excercise** convert this function to OCAML. Also write an `append` function. + Test with simple lists. - datatypeÂ âaÂ treeÂ = Leaf |Â NodeÂ ofÂ âaÂ treeÂ *Â âaÂ *Â âaÂ tree + ConsiderÂ theÂ followingÂ simpleÂ binaryÂ treeÂ type: - (a)Â GiveÂ aÂ SystemÂ FÂ encodingÂ ofÂ binaryÂ trees,Â includingÂ aÂ deï¬nitionÂ ofÂ theÂ typeÂ ÏÂ treeÂ andÂ deï¬nitionsÂ of - theÂ constructorsÂ leafÂ :Â ÏÂ treeÂ andÂ nodeÂ :Â ÏÂ treeÂ âÂ ÏÂ âÂ ÏÂ treeÂ âÂ ÏÂ tree. + typeÂ âaÂ treeÂ = Leaf |Â NodeÂ ofÂ âaÂ treeÂ *Â âaÂ *Â âaÂ tree - (b)Â WriteÂ aÂ functionÂ heightÂ :Â ÏÂ treeÂ âÂ nat.Â YouÂ mayÂ assumeÂ theÂ aboveÂ encodingÂ ofÂ natÂ asÂ wellÂ asÂ deï¬nitions - ofÂ theÂ functionsÂ plusÂ :Â natÂ âÂ natÂ âÂ natÂ andÂ maxÂ :Â natÂ âÂ natÂ âÂ nat. + **Excercise** + Write a function `sumLeaves` that computes the sum of all the + leaves in an int tree. - (c)Â WriteÂ aÂ functionÂ in-orderÂ :Â ÏÂ treeÂ âÂ ÏÂ listÂ thatÂ computesÂ theÂ in-orderÂ traversalÂ ofÂ aÂ binaryÂ tree.Â You + WriteÂ aÂ functionÂ `inOrder`Â :Â ÏÂ treeÂ âÂ ÏÂ listÂ thatÂ computesÂ theÂ in-orderÂ traversalÂ ofÂ aÂ binaryÂ tree.Â You mayÂ assumeÂ theÂ aboveÂ encodingÂ ofÂ lists;Â deï¬neÂ anyÂ auxiliaryÂ functionsÂ youÂ need. -- 2.11.0