***********************************************************************
* 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 PredicateLogic 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              these are
>   | EVar Var			-- variables              "in-line"
>   | Neg IntExp		-- negation               comments,
>   | IntExp :+: IntExp		-- addition               from the "--"
>   | IntExp :-: IntExp		-- subtraction            to the end of
>   | IntExp :*: IntExp		-- multiplication         each line
>   | IntExp :/: IntExp		-- division
>   | IntExp `Rem` IntExp	-- remainder
>   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 :=>:  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 `Rem` e2) s = intExp e1 s `rem` 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 :=>:  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!

> test p = assert p s0

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