Exercises for Chapter 5, Part 2

The answer to Question 5 should be typed as a .txt (text) file. (You do not use any checker tool to validate it.)

Place your answers in a zipped folder and submit to K-State Online.

Questions 1 to 4: Use the checker tool to prove these claims:

1. p -> q, ~q |− ~p

2. q -> r, p -> ~r |− p -> ~q

3. p -> q, ~q |− p -> r

4. (~q) -> (~p) |− p -> q
   (Hint: use Pbc)

Question 5. (Please read to the end to see the exercise.)

Compilers do data-type checking with propositional logic. Here's an example: Say we have this language, with int and array variables and baby functions. Here is a sample program in the language:

# we must declare names, with their types, before using them:
dec int x; 
dec int-array r;
dec int -> int f;
f = fun(int a) return a + 1 end;  # f gets function code
x = 0;                            # x gets an int
r = new int[4];                   # r gets an array
r[x+1] = 1;
x = f(x)

===================================================

PROGRAM ::=  COMMANDSEQUENCE
COMMANDSEQUENCE ::=  COMMAND  |  COMMAND ; COMMANDSEQUENCE  
                 
COMMAND ::=  dec TYPE VAR  |  VAR = EXPR  |  VAR [ EXPR ] = EXPR

EXPR ::=  NUM  |  VAR  |  EXPR + EXPR  |  VAR [ EXPR ]  |  VAR ( EXPR )
       |  new TYPE [ NUM ]
       |  fun ( TYPE  VAR ) return EXPR end

NUM  is a sequence of digits
VAR  is a string beginning with a letter,
       but not 'new', 'int', 'array', 'dec', 'fun', 'return', or 'end'.

TYPE ::=  int  |  TYPE-array  |  TYPE1 -> TYPE2

===================================================

The C# and Java compilers use a type checker to detect in advance some programming errors (the "type errors"). If the type checker determines that a program contains an error, the program is not translated into an .exe or bytecode file.

The type checker is actually a theorem prover for a propositional logic. In the above program, variable x has type int, variable r has type int-array, and function f has type int -> int, and the type checker uses these "premises" to make a "proof" of the program's well-typedness.

Here are the deduction laws for the above language. The laws prove propositions of the form, program-phrase: data-type, that is, ``program-phrase has type data-type''.

===================================================

NOTE: in the rules below,  v  is a variable name (VAR),  e  is an expression phrase (EXPR),
      and  A  is a type (TYPE)


premise: -------------  dec A v  appears, and  v  is a new var name
             v: A

        
          v: A     e: A                      v: A-array    e1: int    e2: A
assign: ------------------     arrayassign: -----------------------------------
             v = e : A                          v[e1] = e2 : A

           
array: ---------------------  n is a NUM
        new A[n] :  A-array  

 
      +--------------------
      | v: A    assumption
      |   ...
      | e: B
      +--------------------
fun: -------------------------------  v is a new var name
      fun (A v) return e :  A —> B



      e1: A —> B     e2: A
call: ----------------------------
            e1(e2) :  B
 

                           e1: int    e2: int    
num: -----------     add: ---------------------
       n : int               e1 + e2 : int 


         v: A-array    e: int
index: ---------------------
             v[e] : A

===================================================

A type checker implements the above deduction rules. Here is the proof that the example program is well-typed:

1. x : int                       premise (dec int x)
2. r : int-array                 premise (dec int-array r)
3. f : int -> int                premise (dec int->int f)

+------------------------------------
|  4.  a : int            assumption
|  5.  1 : int            num
|  6.  a + 1 : int        add 4,5
+------------------------------------
7. fun(int a) return a+1 end :  int -> int      fun 4-6
8. f = fun(int a) return a+1 end : int -> int   assign 3,7

9.  0: int                          num
10. x = 0 : int                     assign 1,9

11.  new int[4] : int-array         array
12.  r = new int[4] : int-array     assign 2,11

13.  1 : int                        num
14.  x + 1 : int                    add 1,13
15.  r[x+1] = 1 : int               arrayassign 2,14,13

16.  f(x) : int                     call 3,1
17.  x = f(x) : int                 assign 1,16

Here is your exercise: Write a proof in the above style that shows this program is well-typed:

dec int-array -> int  g;
dec int-array  b;
b = new int[3];
dec int a;
g = fun(int-array c) return c[a] end;
a = 1;
b[a + a] = a;
a = g(b)