%%% Assignment 5 %%% Out: Wed 17 Oct %%% Due: Wed 24 Oct %%% Author : Brigitte Pientka % % Use tutch to check your implementations in the following problems. % A sample solution looks like this: % % S. Double a Natural Number % % Give a specification and implementation for the function double, % which doubles a natural number. %val double : nat -> nat % Solution: % % specification: % % double : nat -> nat % double 0 = 0 % double sx = ss(double x) % % implementation: val double : nat -> nat = fn x => rec x of f 0 => 0 | f(s x') => s (s (f x')) end; % 1. Boolean functions % % Give specifications and term implementations % for the following usual boolean operations: % % not, and, or, implies, iff, xor (exclusive or). % % val not : bool -> bool % Solution: % % specification: % not: bool -> bool % not true = false % not false = true % % implementation: val not : bool -> bool = fn x => if x then false else true; % val and : bool -> bool -> bool % Solution: % % specification: % and true true = true % false otherwise % % implementation: val and : bool -> bool -> bool = fn x => fn y => if x then y else false; % val or : bool -> bool -> bool % Solution: % % specification: % and false false = false % true otherwise % % implementation: val or : bool -> bool -> bool = fn x => fn y => if x then true else y; % val implies : bool -> bool -> bool % Solution: % % specification: % implies true false = false % true otherwise % % implementation: val implies : bool -> bool -> bool = fn x => fn y => or (not x) y; % val iff : bool -> bool -> bool % Solution: % % specification: % iff true true = true % iff false false = true % false otherwise % % implementation: val iff : bool -> bool -> bool = fn x => fn y => and (implies x y) (implies y x); % val xor : bool -> bool -> bool % Solution: % % specification: % xor true true = false % xor false false = false % true otherwise % % implementation: val xor : bool -> bool -> bool = fn x => fn y => not (iff x y); %{ % 2. Using the function half defined in class, % explicitely compute half 3 half 3 = (fn x => fst (half12 x)) 3 --> fst (half12 3) = fst (fn x => rec x of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end 3) --> fst ( rec (s s s 0) of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x')))) end --> [s s 0/x'] fst ( snd(h x'), s (fst (h x') ) ) = fst ( snd (h (s s 0)), s (fst (h (s s 0)))) --> snd (h (s s 0)) = snd ( fn x => rec x of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end (s s 0) ) --> snd ( rec (s s 0) of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end) --> [s 0/ x'] snd ( snd(h x'), s (fst (h x'))) = snd ( snd (h (s 0)), s (fst (h (s 0)))) --> s (fst (h (s 0))) = s (fst (fn x => rec x of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end (s 0) )) --> s (fst (rec s 0 of h(0)=>(0,0) | h( s x') => (snd(h x'), s (fst (h x') ) ) ) ) --> [ 0 /x'] s (fst (snd(h x'), s (fst (h x') ) ) ) = s ( fst (snd(h 0), s (fst (h 0) ) ) ) --> s ( snd (h 0) ) --> s ( snd ( fn x => rec x of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end 0) ) --> s ( snd ( rec 0 of h(0)=>(0,0) | h( s x')=> (snd(h x'), s (fst (h x'))) end ) ) --> s ( snd (0,0) ) --> s 0 % }% % 3. Recursion on nat % % Give specification and term implementations % for the following functions on natural numbers. % Follow the example of double given in class. % % (factorial) fact : nat -> nat should compute n!, % i.e. the product of the first n+1 numbers except 0 % (set 0! = 1). val plus : nat -> nat -> nat = fn x => fn y => rec x of p 0 => y | p (s x') => s (p x') end; val times : nat -> nat -> nat = fn x => fn y => rec x of t 0 => 0 | t (s x') => plus y (t x') end; val minus : nat -> nat -> nat = fn x => rec x of m 0 => fn y => 0 | m (s x') => fn y => rec y of p 0 => (s x') | p (s y') => m x' y' end end; % val fact: nat -> nat % % specification: % fact 0 = 1 % fact sx = times sx (fact x) % implementation: val fact : nat -> nat = fn x => rec x of f 0 => (s 0) | f (s x') => times (s x') (f x') end; % (equality) eq : nat -> nat -> bool such that % eq n m returns true if and only if n = m. % val eq : nat -> nat -> bool % Solution % specification : % equal 0 0 = true % equal 0 (s y') = false % equal (s x') 0 = false % equal (s x') (s y') = equal x' y' % % implementation val eq : nat -> nat -> bool = fn x => rec x of e 0 => (fn y => rec y of e' 0 => true | e' (s y') => false end) | e (s x') => (fn y => rec y of e' 0 => false | e' (s y') => e x' y' end) end; % (exponentiation) exp : nat -> nat -> nat such that % exp n m is m raised to the n-th power. % val exp : nat -> nat -> nat % Solution: % % specification: % exp 0 m = 1 (note exp 0 0 = 1) % exp (s n') m = times m (exp n' m) % % implementation: val exp : nat -> nat -> nat = fn n => rec n of e 0 => fn m => (s 0) | e (s n') => fn m => times m (e n' m) end; % (even) even: nat -> bool such that % even n is true just in case n is even. % val even: nat -> bool % Solution: % % specifications: % even 0 = true % even (s 0)= false % even ( s s n') = even n' val even12: nat-> bool*bool = fn x => rec x of e 0 => (true, false) | e (s x) => (snd (e x), not(fst(e x))) end; val even: nat -> bool = fn x => fst ( even12 x) ; % % 4. Lists % % Specify and implement the following operations on lists. % % drop l i % returns what is left after dropping the first i elements of the list l. % % val drop : tau list -> nat -> tau list % Solution: % specification: % drop l 0 = l % drop nil x = nil % drop (h::t) (s x) = drop t x % %implementation val drop : tau list -> nat -> tau list = fn l => rec l of d nil => fn i => nil | d (h::t) => fn i => rec i of d' 0 => h::t | d' (s i') => d t i' end end; % take i l % returns the first i elements of the list l. % return nil in any other case % val take : nat -> tau list -> tau list % Solution: % % specifications: % take 0 l = l % take (s x) (h::t) = h :: (take x t) iff length t >= x val take' : nat -> tau list -> tau list -> tau list = fn n => rec n of f 0 => fn l => fn acc => acc | f (s m) => fn l => rec l of g nil => fn acc => nil | g (x::xs) => fn acc => f m xs (x::acc) end end; val take : nat -> tau list -> tau list = fn n => fn l => take' n l nil; %{ % 5. Expressions % % Define an inductive data type express of arithmetical expressions % over natural numbers, the terms of which are expressions like % 2*(3+1) + (4+22)*(3+9), etc. % % Give formation, introduction, and elimination rules % involving two constructors Pxy and Txy (for plus and times). % We will also define a base constructor numb which converts a natural number into an expression. Formation - ----------- eF express : type Introduction - G |- x : nat --------------------- expressVI G |- numb x : express G |- x : express G |- y : express -------------------------------------- expressPI G |- P(x,y) : express G |- x : express G |- y : express ------------------------------------- expressTI G |- T(x,y) : express Elimination - G |- t : tau G , n : nat |- t_n : tau G ,x : express, y : express, f(x) : tau, f(y) : tau |- t_P : tau G ,x : express, y : express, f(x) : tau, f(y) : tau |- t_T : tau ------------------------------------------------------------- expressE G |- rec t of f(numb n) => t_n | f(P(x,y)) => t_P | f(T(x,y)) => t_T end : tau % note : % where t_n represents the base case; % t_n can never contain any occurrences of f as there is no operation which allows us % to take a natural number and % return an expression; % % where t_P may mention x,y, f(x), f(y) but no other occurences of f % and similarly for t_T. % % % Give specification and implementations for each of the following functions. % % count e is the number of numerals in the expression e % % count : express -> nat % Solution : % % specification: % count (Numb n) = 1 % count (P(x,y))= plus (count x) (count y) % count (T(x,y))= plus (count x) (count y) % % implementation: count : express -> nat = fn t => rec t of c(Numb n) => 1 | c(P(x,y))=> plus (c x) (c y) | c(T(x,y))=> plus (c x) (c y) end; % val e is the value of the expression upon evaluation of % Pxy as x+y and Txy as x*y % val : express -> nat % Solution: % % specification: % eval (Numb n) = n % eval (P(x,y)) = plus (eval x) (eval y) % eval (T(x,y)) = times (eval x) (eval y) % % implementation: val eval : express -> nat = fn t => rec t of v (Numb n) => n | v (P(x,y))=> plus (v x) (v y) | v (T(x,y))=> times (v x) (v y) end; }%