%%% Assignment 4 %%% Out: Fr 5 Oct %%% Due: Fr 12 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: % % a) specification: % % double : nat -> nat % double 0 = 0 % double sx = ss(double x) % % b) implementation: val double : nat -> nat = fn x => rec x of f 0 => 0 | f(s x') => s (s (f x')) end; % 1. Boolean functions (20 points) % % Give specifications and term implementations % for the following usual boolean operations: % % iff, xor (exclusive or), nand. % % val iff : bool -> bool -> bool % Solution: % % a) specification: % % b) implementation: % val xor : bool -> bool -> bool % Solution: % % a) specification: % % b) implementation: % val nand : bool -> bool -> bool % Solution: % % a) specification: % b) implementation: %{2. Maximum function (30 points) % % Implement the maximum function max : nat -> nat -> nat % that returns the maximum of two natural numbers. % Implement first the auxiliary function % x greater or equal to y. % a) Specification of greater % b) Implementation of greater % a) Specification of maximum function % b) Implementation of maximum function %{ % 3. Expressions (50 points) % % Following the development for defining numbers inductively, 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). % Also define a constructor numb which converts a natural number % into an expression. Formation Rules - INSERT IT HERE Introduction Rule - INSERT IT HERE Elimination - INSERT IT HERE % Using this extension you defined, give specification and % implementations for each of the following functions. % % count e is the number of numerals in the expression e % % count : expr -> nat % Solution : % % a) specification: % % b) implementation: % Using this extension and functions we have defined % for plus and times, define a function which evaluates % an arithmetic expression to a natural number n % We interpret Pxy as x+y and Txy as x*y % val : expr -> nat % Solution: % % a) specification: % % b) implementation: }%