ex-types

This shows you the differences between two versions of the page.

— |
ex-types [2015/10/08 15:20] (current) |
||
---|---|---|---|

Line 1: | Line 1: | ||

+ | ====== LiP assignment #5 ====== | ||

+ | |||

+ | ===== 1. Rational numbers ===== | ||

+ | |||

+ | Write a record type ''num'' to represent [[wp>Rational_number|rational numbers]], and the functions: | ||

+ | * ''add_num: num -> num -> num'', that adds two rational numbers. | ||

+ | * ''leq_num: num -> num -> bool'', that compares two rational numbers x, y. It returns ''true'' if x≤y, otherwise it returns ''false''. | ||

+ | |||

+ | //Warning//: you are not allowed to use floats! | ||

+ | |||

+ | \\ | ||

+ | |||

+ | ===== 2. Card game ===== | ||

+ | |||

+ | Assume we want to model a card game, played with a deck of 40 cards with French suites | ||

+ | (spades, hearts, diamonds, clubs). | ||

+ | A set of cards if a value of type ''deck'', where: | ||

+ | <code ocaml> | ||

+ | # type suit = Spades | Hearts | Diamonds | Clubs;; | ||

+ | # type card = Card of int * suit;; | ||

+ | # type deck = Deck of card list;; | ||

+ | </code> | ||

+ | |||

+ | Of course, not all values of type ''card'' actually represent a card, since cards only make sense | ||

+ | when the integer component is comprised between 1 (Ace) and 10 (King). | ||

+ | |||

+ | Write the following functions on decks: | ||

+ | * ''deck_complete: deck -> bool'', tells whether the given deck is correct and complete, i.e. it is composed by 40 (well-formed) cards, all different. | ||

+ | * ''newdeck : unit -> deck'', produces a new, complete deck of cards //(Note: enumerating all the cards is not permitted.)// | ||

+ | * ''partition : deck -> deck * deck * deck * deck'', partitions the given deck of cards into four decks, which are composed by cards of the same suit. | ||

+ | |||

+ | \\ | ||

+ | |||

+ | ===== 3. Queues ===== | ||

+ | |||

+ | Define a polymorphic type '''a queue'' for representing queues, and specify the functions: | ||

+ | * ''enqueue: 'a -> 'a queue -> 'a queue'', that inserts an element in the queue. | ||

+ | * ''dequeue: 'a queue -> 'a queue'', that removes an element from the queue. | ||

+ | * ''isempty: 'a queue -> bool'', that returns ''true'' if the queue is empty. | ||

+ | * ''peek: 'a queue -> 'a partial'', that peeks the first element from the queue. | ||

+ | |||

+ | \\ | ||

+ | |||

+ | ===== 4. Evaluating arithmetic expressions ===== | ||

+ | |||

+ | Let us extend the syntax of arithmetic expressions, so to also deal with boolean expressions: | ||

+ | <code ocaml> | ||

+ | # type exp = | ||

+ | True | ||

+ | | False | ||

+ | | Not of exp | ||

+ | | Or of exp*exp | ||

+ | | And of exp*exp | ||

+ | | Const of int | ||

+ | | Var of string | ||

+ | | Sum of exp * exp | ||

+ | | Sub of exp * exp | ||

+ | </code> | ||

+ | |||

+ | Write the evaluation function for such expressions. | ||

+ | Since now the results can either be of type ''int'' or type ''bool'', the return type of the | ||

+ | ''eval'' function should be a variant type, e.g. | ||

+ | <code ocaml> | ||

+ | # type result = Bool of bool | Int of int | ||

+ | |||

+ | # let rho = [("x",Int 3); ("y", Bool true)];; | ||

+ | |||

+ | # eval (Sum(Var "x", Const 5)) rho;; | ||

+ | - : result = Int 8 | ||

+ | </code> | ||

+ | |||

+ | You shall raise an exception when trying to mix integers with booleans. For instance: | ||

+ | <code ocaml> | ||

+ | # eval (Sum(Var "x", Var "y")) rho;; | ||

+ | |||

+ | Exception: Failure "Type mismatch". | ||

+ | </code> | ||

+ | |||

+ | \\ | ||

+ | |||

+ | |||

+ | ===== 5. Simple type checking ===== | ||

+ | |||

+ | Consider the language of logic and arithmetic expressions defined by the following abstract syntax: | ||

+ | <code ocaml> | ||

+ | type exp = | ||

+ | Const of int | ||

+ | | Sum of exp * exp | ||

+ | | True | ||

+ | | False | ||

+ | | Not of exp | ||

+ | | And of exp*exp | ||

+ | | Ifthen of exp*exp*exp;; | ||

+ | </code> | ||

+ | |||

+ | Then, consider the following tagged union: | ||

+ | <code ocaml> | ||

+ | type t = TInt | TBool | TErr;; | ||

+ | </code> | ||

+ | |||

+ | An expression ''e'' has type: | ||

+ | * ''TInt'', iff | ||

+ | * e = Const v for some v, or | ||

+ | * e = Sum(e1,e2) and both e1 and e2 have type ''TInt'', or | ||

+ | * e = Ifthen(e0,e1,e2) and e0 has type ''TBool'' and both e1 and e2 have type ''TInt'' | ||

+ | * ''TBool'' iff | ||

+ | * e = True, or | ||

+ | * e = False, or | ||

+ | * e = Not(e') and e' has type ''TBool'', or | ||

+ | * e = And(e1,e2) and both e1 and e2 have type TBool, or | ||

+ | * e = Ifthen(e0,e1,e2) and both e0, e1 and e2 have type ''TBool''. | ||

+ | * ''TErr'', in all the other cases. | ||

+ | |||

+ | Write a function ''typecheck: exp -> t'' such that ''typecheck e'' infers the type of ''e''. | ||

+ | |||

+ | \\ | ||

+ | |||

+ | ===== 6. Lambda calculus substitutions ===== | ||

+ | |||

+ | Consider the language of //λ-terms// defined by the following abstract syntax | ||

+ | (where x is a //variable//): | ||

+ | |||

+ | t ::= x | t t | λx. t | ||

+ | |||

+ | For instance, a valid λ-term is (λx.(x (λz.y z))) x. | ||

+ | |||

+ | Write a type ''term'' to represent λ-terms. Assume that variables are represented as strings. | ||

+ | |||

+ | |||

+ | The //free variables// fv(t) of a term t are defined inductively a follows: | ||

+ | * fv(x) = {x} | ||

+ | * fv(t t') = fv(t) ∪ fv(t') | ||

+ | * fv(λx. t) = fv(t) \ {x} | ||

+ | |||

+ | For instance, fv(%%(%%λx.(x (λz.y z))) x) = {x,y}. | ||

+ | |||

+ | Write a function ''fv: term -> string list'' such that ''fv t'' evaluates to the | ||

+ | set (i.e. a list without repetitions) fv(t). | ||

+ | |||

+ | |||

+ | Given two terms t and t', and a variable x, the //substitution// t{t'/x} is defined inductively as follows: | ||

+ | * x{t'/x} = t' | ||

+ | * y{t'/x} = y, if y≠x | ||

+ | * (t s){t'/x} = t{t'/x} s{t'/x} | ||

+ | * (λx. t){t'/x} = λx. t | ||

+ | * (λy. t){t'/x} = λy. t{t'/x} if y≠x and y∉fv(t') | ||

+ | * otherwise, t{t'/x} is undefined. | ||

+ | |||

+ | For instance, (%%(%%λx.(x (λz.y z))) x){y y/x} = (λx.(x (λz.y z))) (y y), | ||

+ | while (%%(%%λx.(x (λz.y z))) x){z/y} is undefined. | ||

+ | |||

+ | Write a function ''subst: string -> term -> term -> term '' such that | ||

+ | ''subst x t' t'' evaluates to t{t'/x} when such substitution is defined, | ||

+ | and fails otherwise. | ||

+ | |||

+ | |||

+ | Two λ-terms are //alpha-equivalent// if they are equal up-to renaming of | ||

+ | non-free variables. | ||

+ | |||

+ | For instance, (%%(%%λx.(x (λz.y z))) x) and (%%(%%λz.(z (λz.y z))) x) are alpha-equivalent, | ||

+ | while (%%(%%λx.(x (λz.y z))) x) and (%%(%%λx.(x (λy.y y))) x) are not | ||

+ | (because renaming z as y captures the free occurrence of y). | ||

+ | |||

+ | Write a function ''alpha: term -> term -> bool'' such that ''alpha t v'' evaluates to true | ||

+ | iff the λ-terms t and v are alpha-equivalent. | ||

+ | |||

+ | \\ | ||

+ | ===== 7. Binary search trees ===== | ||

+ | |||

+ | A binary search tree is a tree which enjoys the following properties: | ||

+ | * each node has a search "key" and at most two children | ||

+ | * each key is present at most once in the tree | ||

+ | * for any node, the key is greater than the key of every node in the subtree rooted at the left child and less than every key in the subtree rooted at the right child. | ||

+ | |||

+ | Binary search trees are values of the following polymorphic variant type: | ||

+ | <code ocaml> | ||

+ | # type 'a bstree = Empty | Node of 'a * 'a bstree * 'a bstree | ||

+ | </code> | ||

+ | |||

+ | The exercise asks for implementing the following functions: | ||

+ | <code ocaml> | ||

+ | member : 'a -> 'a bstree -> bool | ||

+ | height : 'a bstree -> int | ||

+ | insert : 'a -> 'a bstree -> 'a bstree | ||

+ | inorder : 'a bstree -> 'a list | ||

+ | sanitycheck : 'a bstree -> bool | ||

+ | maptree : ('a -> 'b) -> 'a bstree -> 'b bstree | ||

+ | </code> | ||

+ | |||

+ | We now briefly discuss the expected behaviour of these functions, | ||

+ | with the help of some examples. | ||

+ | |||

+ | The function ''member'' reports whether or not a key occurs in a tree. | ||

+ | <code ocaml> | ||

+ | # member 3 (Node(7, Node(4, Empty, Empty), Empty));; | ||

+ | - : bool = false | ||

+ | |||

+ | # member 4 (Node(7, Node(4, Empty, Empty), Empty));; | ||

+ | - : bool = true | ||

+ | </code> | ||

+ | |||

+ | The funtion ''height'' computes the length of the longest path in the tree. | ||

+ | <code ocaml> | ||

+ | # height Empty;; | ||

+ | - : int = 0 | ||

+ | |||

+ | # height (insert 1 (insert 2 (insert 3 (insert 4 Empty))));; | ||

+ | - : int = 4 | ||

+ | </code> | ||

+ | |||

+ | The function ''insert'' inserts a new key into the tree, unless it already exists. | ||

+ | The function will construct and return a | ||

+ | new binary search tree, which has the inserted key (i.e. there are no side effects) | ||

+ | <code ocaml> | ||

+ | # insert 3 (Node(7, Node(4, Empty, Empty), Empty));; | ||

+ | - : bstree = Node (7, Node (4, Node (3, Empty, Empty), Empty), Empty) | ||

+ | |||

+ | # insert 4 (Node(7, Node(4, Empty, Empty), Empty));; | ||

+ | - : bstree = Node (7, Node (4, Empty, Empty), Empty) | ||

+ | |||

+ | # insert 4 Empty;; | ||

+ | - : bstree = Node (4, Empty, Empty) | ||

+ | </code> | ||

+ | |||

+ | The function ''inorder'' produces a list of the keys visited in a in-order traversal. | ||

+ | Given a binary tree, an in-order traversal consists of executing an in-order traversal on the root's left child (if present), then visiting the root, then executing an in-order traversal on the root's right child (if present). Thus, all the left descendents of the root are visited before the root, and the root is visited before any of its right descendents. | ||

+ | <code ocaml> | ||

+ | # inorder (insert 4 (insert 8 (insert 2 Empty)));; | ||

+ | - : int list = [2; 4; 8] | ||

+ | |||

+ | # inorder (insert 2 (insert 4 (insert 8 Empty)));; | ||

+ | - : int list = [2; 4; 8] | ||

+ | </code> | ||

+ | |||

+ | The ''sanitycheck'' function checks if a tree is indeed a binary search tree: that is, | ||

+ | if each key is present at most once in the tree, and that for each node, | ||

+ | every key in the left child is lower than the key for the node, | ||

+ | and every key in the right child is greater. (//Hint:// can you use ''inorder''?) | ||

+ | <code ocaml> | ||

+ | # sanitycheck (insert 4 (insert 8 (insert 2 Empty)));; | ||

+ | - : bool = true | ||

+ | |||

+ | # sanitycheck Empty;; | ||

+ | - : bool = true | ||

+ | |||

+ | # sanitycheck (Node (4, Node (4, Empty, Empty), Empty));; | ||

+ | - : bool = false | ||

+ | </code> | ||

+ | |||

+ | The function ''maptree'' applies a function to each key of a tree. | ||

+ | <code ocaml> | ||

+ | # let square x = x * x;; | ||

+ | val square : int -> int = <fun> | ||

+ | |||

+ | # maptree square Node (4, Node (3, Empty, Empty), | ||

+ | Node (7, Node (6, Empty, Empty), Node (9, Empty, Empty)));; | ||

+ | - : bstree = Node (16, Node (9, Empty, Empty), | ||

+ | Node (49, Node (36, Empty, Empty), Node (81, Empty, Empty))) | ||

+ | </code> | ||

ex-types.txt · Last modified: 2015/10/08 15:20 (external edit)