%%% 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!