% % COMP 426: FALL 2007 % % Assignment 4 SOLUTIONS % % (Questions 1 and 2 only) % % Prepared by Maja Frydrychowicz % %-------------------------------------------------------------------- % ------------------------------------------------------------------- % Question 1: % Give specifications and term implementations for the following % boolean operations: iff, xor, nand. % ------------------------------------------------------------------- % ------ auxiliary functions ------ val not: bool -> bool = fn x => if x then false else true; % ------ IFF -------- %{ specification: iff true y = y iff false y = not y implementation: }% % version 1 val iff1: bool -> bool -> bool = fn x => fn y => if x then y else if y then false else true; % version 2 val iff2: bool -> bool -> bool = fn x => fn y => if x then y else not y; % ------ XOR -------- %{ specification: xor true y = not y xor false y = y implementation:}% % version 1 val xor1: bool -> bool -> bool = fn x => fn y => if x then not y else y; % version 2 val xor2: bool -> bool -> bool = fn x => fn y => if x then if y then false else true else y; % ------ NAND -------- %{ specification: nand true y = not y nand false y = true implementation:}% % version 1 val nand1: bool -> bool -> bool = fn x => fn y => if x then not y else true; % version 2 val nand2: bool -> bool -> bool = fn x => fn y => if x then if y then false else true else true; % ------------------------------------------------------------------- % Question 2: % Implement the maximum function max: nat -> nat -> nat that returns % the maximum of two natural numbers. Implement first auxiliary % function which tests whether x is greater or equal to y. % ------------------------------------------------------------------- % ------ MAXAUX -------- % % (maxaux x y) tests whether x is greater or equal to y % %{ specification: maxaux 0 0 = true maxaux 0 y = false maxaux x 0 = true maxaux s(x) s(y) = maxaux x y implementation:}% val maxaux: nat -> nat -> bool = fn x => rec x of a 0 => fn y => rec y of b 0 => true | b (s y') => false end | a (s x') => fn y => rec y of c 0 => true | c (s y') => a x' y' end end; % ------ MAX -------- val max: nat -> nat -> nat = fn x => fn y => if maxaux x y then x else y;