Exercises for Chapter 5, part 2

10 points. Due Friday, October 30

The answers to Questions 1-4 should be prepared as .ndp files. The answer to Question 5 is just a .txt (text) file. Place your answers in a zipped folder and submit to K-State Online.

Use the natural-deduction-proof checker to prove each of these sequents:

1. p v q, r, p -> ~r |- q (Hint: use _|_e and ~e)

2. p -> s, q -> (~s) |- ~(p ^ q) (Hint: use ~i and ~e)

3. q -> ~p |- p -> ~q

4. (~p) -> q, ~q |- p (use Pbc)

5. Compilers do data-type checking with propositional logic. Here's how it works: Say we have this mini-programming language. Here is its grammar:

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

PROGRAM ::=  COMMANDSEQUENCE
COMMANDSEQUENCE ::=  COMMAND  |  COMMAND ; COMMANDSEQUENCE
COMMAND ::=  VAR = EXPR |  print VARIABLE  |  def VAR ( VAR ) : return EXPR
EXPR ::=  NUMERAL  |  VAR  |  EXPR + EXPR 
       |  ( EXPR, EXPR ) |  EXPR [0]  |  EXPR [1]
       |  VAR ( EXPR )
NUMERAL  is a sequence of digits from the set, {0,1,2,...,9} 
VAR  is a string beginning with a letter, not  'print' or 'def' or 'return'

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

Here is some explanation: A program is a sequence of one or more commands. A command can be an assignment, a print, or a function definition. Here are the forms of expressions:

0,1,2,... are expressions that have type int
a variable name that is already assigned is an expression.
addition, +, combines two ints to make a new int
expressions e1 and e2 can be made into a pair expression, (e1,e2) (If you wish, think of a pair expression as a two-element array.) A pair expression has a data type that is the pair type of its two elements. (See below.)
a pair expression, e, can be indexed to extract its elements by e[0] and e[1].
a function call, f(e), is an expression that returns an answer.

Now we can say more about the forms of commands:

when e is an expression and x is a variable name, then x = e is an assignment to x, which takes on the type that e has.
when e is an expression that refers to a variable n, then def f(n): return e is a function that we can call by stating, f(e'), for some other expression, e'.
when e is an expression, print e prints it.

Here is a sample program in the language: x = 2 def d(n): return x + n ; p = (d(2), x); print p[0]
When activated, the program does these steps:

it assigns 2 to x
it binds ("assigns") the code, (n): return x + n, to the name, d
it computes d(2), which computes to 2 + 2 which computes to 4; it then assigns the pair, (4,2), to p (because x names 2).
it computes p[0], that is, 4, and prints it.

Not all programs in this language are sensible, e.g.,

p = (2,y);
print  4 + p

(Variable y is uninitialized and you cannot add an int to a pair.)

Languages like Java and C# use a compiler with a type checker to see if such programs have any hope of executing correctly. (If not, then the programs are not translated into .exe files.) The type checker is actually a theorem-prover program for a logic of data types. Here are the data-type deduction laws for the mini-language, which prove propositions of the form, program-phrase : data-type.

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

                                                     e1: int    e2: int
int: ---------   ---------  ---------  ...    add:  --------------------
       0: int      1: int     2:int                     e1 + e2 : int


        e1: P     e2: Q                    e: P ^ Q                 e: P ^ Q
pair: -----------------------   index0: ---------------   index1: -------------
         (e1,e2) : P ^ Q                   e[0]: P                  e[1]: Q


            e: P                                     x = e : P
assign: --------------- x is a brand      lookup: ---------------
           x = e :  P     new name                    x : P

 
      ... x: P  assume
      ... e: Q                                   
def: ------------------------------- f and x are brand new names
       def f(x): return e : P -> Q 


       def f(x): return e : P -> Q        e': P
call: ----------------------------------------------
                  f(e') : Q
         

           e : P
print: -----------------
        print e : P

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

For example, we use the int law to deduce that 1. 2 : int int
that is, 2 has int type. Then, we can use the assign law to deduce that 2. x = 2 assign 1
showing that the assigment, x = 2, is well-typed and executable.

In this manner, the type checker builds a proof that shows that each line of the program is well-typed (a "fact") according to the deduction laws of the type logic. Here is the proof that the above program,

x = 2
def d(n): return x + n ;
p = (d(2), x);
print p[0]

is well-typed and should be allowed to execute: 1. 2 : int int 2. x = 2 assign 1 ... 3. n: int assumption ... 4. x: int lookup 2 ... 5. x + n: int add 4,3 6. def d(n): return x + n : int -> int def 3-5 7. d(2): int call 6,1 8. x: int lookup 2 9. (d(2), x) : int ^ int pair 7,8 10. p = (d(2),x) : int ^ int assign 9 11. p : int ^ int lookup 10 12. p[0] : int index0 11 13. print p[0] : int print 12
Notice how the complete proof is broken into four groups, one group for each line of the program. This is how type checking works.

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

def g(n): return (n, n + 2);
b = g(4)[1];
print b