*************************************************************************
* CS-430/530                                                            *
*                                                                       *
* Problem Set 1 Solution                                                *
*                                                                       *
* Prepared by Paul Hudak                                                *
* September 15, 2007                                                    *
*************************************************************************


Problem 1
========================

   P(a,b) == Exists m . m > 0 /\ a*m = b

   Q(a,b,c) == P(a,b) /\ P(a,c)

a) PRIME(b) == not Exists a . (a /= b) /\ (a /= 1) /\ P(a,b)

b) GCD(a,b,c) == Q(a,b,c) /\ not Exists a' . a'>a /\ Q(a',b,c)

c) FERMAT = not (Exists a . Exists b . Exists c . Exists n . n > 2 /\ a^n + b^n = c^n) 


Problem 4
========================

For exclusive or:

a) We need to extend <assert> with a new term:

   <assert> ::= ... 
              | <assert> xor <assert>       

b) Semantic equation:

   [[ e0 xor e1 ]] s = [[ e0 ]] s XOR [[ e1 ]] s          

c) Free Variable:

   FV(e0 xor e1) = FV(e0) U FV(e1)

d) Substitution rule:

   (e0 xor e1) / del = e0/del xor e1/del


For exponentiation operator:

a) We need to extend <intexp> with a new term:

   <intexp> ::= ... 
              | <intexp> ^ <intexp>

b) Semantic equation:

   [[ e0 ^ e1 ]] s = [[ e0 ]] s ^ [[ e1 ]] s

c) Free Variable:

   FV(e0 ^ e1) = FV(e0) U FV(e1)

d) Substitution rule:

   (e0 ^ e1) / del = e0/del ^ e1/del


For Sigma (Summation):

a) We need to extend <intexp> with a new term:

   <intexp> ::= ...
              | Sig <var>: <intexp> to <intexp> . <intexp>

   Or, in Haskell:

   data IntExp = ...
               | Sigma Var IntExp IntExp IntExp

b) Semantic equation:

                                  [[e2]]s
   [[ Sig v: e1 to e2 . e]] s =    SUM     [[e]] [s | v:n]
                                n = [[e1]]s

   Or, in Haskell, using list comprehensions:

   intExp (Sigma v e1 e2 e) s =
      sum [ intExp e (extend s v n) | n <- [intExp e1 s .. intExp e2 s] ]

c) Free variables:

   FV (Sig v: e1 to e2 . e) = FV(e1) U FV(e2) U (FV(e) - {v})

d) Substitution:

   (Sig v: e1 to e2 . e) / del
    = Sig vnew: (e1/del) to (e2/del) . (e / [del | v : vnew])

    where vnew is any ("fresh") variable that is not an element of:

    BigUnion FV(del u) for each u in FV(e1) U FV(e2) U FV(e) - {v}


The interpreter below has been modified to reflect the above.

***********************************************************************
* A realization of Reynolds' syntax and semantics of Predicate Logic, *
* from Chapter 1 of the text.                                         *
***********************************************************************

Written by Paul Hudak.

This module is written in the "literate Haskell" style, in which
comments / documentation may appear freely, but lines of program code
must be preceded by a ">".

> module PS1Soln where

It is a good idea to name your module the same as your file (but
without the file extension).  Literate Haskell files have extension
.lhs and non-literate ones have extension .hs.

SYNTAX
======

Syntax of expressions:

> data IntExp = 
>     EInt Integer                   -- constants
>   | EVar Var                       -- variables
>   | Neg IntExp                     -- negation 
>   | IntExp :+: IntExp              -- addition 
>   | IntExp :-: IntExp              -- subtraction    
>   | IntExp :*: IntExp              -- multiplication 
>   | IntExp :/: IntExp              -- division
>   | IntExp :^: IntExp              -- exponentiation
>   | IntExp `Rem` IntExp            -- remainder
>   | Sigma Var IntExp IntExp IntExp -- summation
>   deriving (Eq, Show)              -- allows comparison and printing

Note that ordinary constructors must begin with a capital letter
(EInt, Evar, Neg, and Rem), and infix constructors must begin with a
colon (:+:, :-:, etc.).

Also, any Haskell function or constructor may be turned into an infix
function or constructor by enclosing it in backward tickmarks.  Thus
the next-to-the-last line above is equivalent to:

    | Rem IntExp IntExp         -- remainder

Syntax of assertions:

> data Assert =
>     ATrue | AFalse            -- constant
>   | IntExp :=:  IntExp        -- equality
>   | IntExp :/=: IntExp        -- inequality
>   | IntExp :<:  IntExp        -- less than
>   | IntExp :<=: IntExp        -- less than or equal
>   | IntExp :>:  IntExp        -- greater than
>   | IntExp :>=: IntExp        -- greater than or equal
>   | Not Assert                -- negation
>   | Assert :/\:  Assert       -- conjunction (and)
>   | Assert :\/:  Assert       -- disjunction (or)
>   | Assert `Xor` Assert       -- exclusive or (xor)
>   | Assert :=>:  Assert       -- implication
>   | Assert :<=>: Assert       -- if and only if
>   | Forall Var Assert         -- universal quantification
>   | Exists Var Assert         -- existential quantification
>   deriving (Eq, Show)

Variables are just strings:

> type Var = String             -- a type synonym

Type synonyms just give new names to existing types.  So anywhere in
this module, String can be substituted wherever Var appears, without
changing the meaning.

States
======

States (really, environments) map variables to integers:

> type State = Var -> Integer   -- another type synonym

We can extend states using function variation:

> extend :: State -> Var -> Integer -> State
> extend s v i v' = if v == v' then i else s v'

So "extend s v i" is equivalent to "[s | v:i]" in Reynolds.

If you are confused by the definition of "extend", remember that its
type can also be written:

  extend :: (Var -> Integer) -> Var -> Integer -> (Var -> Integer)

which, because of right associativity of "->" (just as in Reynolds),
is equivalent to:

  extend :: (Var -> Integer) -> Var -> Integer -> Var -> Integer

SEMANTICS
=========

Semantic function for expressions:

> intExp :: IntExp -> State -> Integer
>
> intExp (EInt i)          s = i
> intExp (EVar v)          s = s v
> intExp (Neg e)           s = - intExp e s
> intExp (e1 :+: e2)       s = intExp e1 s + intExp e2 s
> intExp (e1 :-: e2)       s = intExp e1 s - intExp e2 s
> intExp (e1 :*: e2)       s = intExp e1 s * intExp e2 s
> intExp (e1 :/: e2)       s = intExp e1 s `div` intExp e2 s
> intExp (e1 :^: e2)       s = intExp e1 s ^ intExp e2 s
> intExp (e1 `Rem` e2)     s = intExp e1 s `rem` intExp e2 s
> intExp (Sigma v e1 e2 e) s = sum [ intExp e (extend s v n) 
>                                    | n <- [intExp e1 s .. intExp e2 s] ]

Semantic function for assertions:

> assert :: Assert -> State -> Bool
>
> assert ATrue  s = True
> assert AFalse s = False
> assert (e1 :=:  e2)  s = intExp e1 s == intExp e2 s
> assert (e1 :/=: e2)  s = intExp e1 s /= intExp e2 s
> assert (e1 :<:  e2)  s = intExp e1 s <  intExp e2 s
> assert (e1 :<=: e2)  s = intExp e1 s <= intExp e2 s
> assert (e1 :>:  e2)  s = intExp e1 s >  intExp e2 s
> assert (e1 :>=: e2)  s = intExp e1 s >= intExp e2 s
> assert (Not p)       s = not (assert p s)
> assert (p1 :/\:  p2) s = assert p1 s && assert p2 s
> assert (p1 :\/:  p2) s = assert p1 s || assert p2 s
> assert (p1 `Xor`  p2) s = assert p1 s `xor` assert p2 s
>                           where xor a b = a && (not b) || b && (not a)
> assert (p1 :=>:  p2) s = if assert p1 s then assert p2 s else True
> assert (p1 :<=>: p2) s = if assert p1 s then assert p2 s
>                          else not (assert p2 s)

The treatment of the final two cases -- universal and existential
quantification -- is problematical, because deciding the validity of a
universally or existentially quantified predicate over integer
arithmetic is semi-decideable.  But let's at least write a
"diagonalizing" algorithm:

> assert (Forall v p) s =
>   and (map f (interleave [0,1..] [-1,-2..]))
>   where f i = assert p (extend s v i)
>
> assert (Exists v p) s =
>   or  (map f (interleave [0,1..] [-1,-2..]))
>   where f i = assert p (extend s v i)

The expression [0,1..] is special Haskell syntax that denotes the
infinite list [0, 1, 2, 3, 4, 5, ...].  Similarly, [-1,-2..] denotes
the infinite list [-1, -2, -3, -4, -5, ...].

These functions are pre-defined in Haskell:

and :: [Bool] -> Bool
or  :: [Bool] -> Bool
map :: (a->b) -> [a] -> [b]

whereas "interleave" is defined here:

> interleave :: [a] -> [a] -> [a]
> interleave (x:xs) (y:ys) = x : y : interleave xs ys

A list [1,2,3] in Haskell can also be written 1:2:3:[].  So a pattern
(x:xs) matches any list with at least one element, binding x to the
first element, and xs to the rest of the list.

Note that "assert (Forall v p) s" will eventually return False if the
answer is in fact False, but will not terminate if the answer is True.
Similarly, "assert (Exists v p) s" will eventually return True if the
answer is in fact True, but will not terminate if the answer is False.

EXAMPLES
========

Initial state that maps all variables to zero:

> s0 :: State
> s0 v = 0

> e1,e2 :: IntExp
> e1 = EInt 15 :+: EInt 27
> e2 = e1 :/: EInt 6

In Haskell, ordinary function or constructor application always has
higher precedence than any infix operator, so "EInt 15 :+: EInt 27" is
parsed properly as "(EInt 15) :+: (EInt 27)".

> p1,p2,p3 :: Assert
> p1 = e1 :>: e2                                -- True                 
> p2 = Forall "x" (EVar "x" :/=: EInt 1000)     -- False
> p3 = Exists "x" (EVar "x" :=:  EInt 1000)     -- True
> p4 = Forall "x" (EVar "x" :=:  EVar  "x")     -- doesn't terminate!
> p5 = Exists "x" (EVar "x" :/=: EVar  "x")     -- doesn't terminate!

> testI e = intExp e s0
> testA p = assert p s0

At the GHCi prompt, you can type "testA p1" to run p1, "testI e2" to
run e2, and so on.  If you type "testA p4" or "testA p5" the program
will get stuck in a loop -- use Cntrl-C to break out of it.