%%% Assignment 5 %%% Out: Wed 17 Oct %%% Due: Wed 24 Oct % % 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 f0 => 0 | f(sx') => ss(fx') 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 val and : bool -> bool -> bool val or : bool -> bool -> bool val implies : bool -> bool -> bool val iff : bool -> bool -> bool val xor : bool -> bool -> bool % 2. Using the function half defined in class, % explicitely compute half3. % % 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 fact : nat -> nat % (equality) eq : nat -> nat -> bool such that % eq n m returns true if and only if n = m. val eq : nat -> nat -> bool % (exponentiation) exp : nat -> nat -> nat such that % exp n m is m raised to the n-th power. val exp : nat -> nat -> nat % (even) even: nat -> bool such that % even n is true just in case n is even. val even: nat -> bool % % 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 % 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 %{ % 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). % % Give specification and implementations for each of the following functions. % % count e is the number of numerals in the expression e count : express -> nat % val e is the value of the expression upon evaluation of % Pxy as x+y and Txy as x*y val : express -> nat }% % Have fun!