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
(Hint: use ~i and ~e)
2. q -> r, p -> ~r |− p -> ~q
3.
p -> q, ~q |− p -> r
(Hint: use ~e and ⊥e)
4.
(~q) -> (~p) |− p -> q
(Hint: use Pbc)
Question 5. (Please read to the end to see your exercise.)
Compilers do data-type checking with propositional
logic. Here's how:
Say we have this mini-programming language, with int and array variables,
assignments, and
baby functions. Here is a sample program in the language:
new int x; # allocates one cell and names it x
new int[4] r; # allocates an array of 4 cells, names it r
x = 0;
def f(int a) : return a + 1 end; # defines function f
r[x+1] = 1; # assigns to a cell of r
x = f(x) # calls f and assigns result to x
Here is the language's grammar; it lists all the legal syntax combinations:
===================================================
PROGRAM ::= COMMANDSEQUENCE
COMMANDSEQUENCE ::= COMMAND | COMMAND ; COMMANDSEQUENCE
# that is, one or more COMMANDs
COMMAND ::= new TYPE VAR
| new TYPE [ NUM ] VAR
| def VAR ( TYPE VAR ) return EXPR end
| VAR = EXPR
| VAR [ EXPR ] = EXPR
EXPR ::= NUM | VAR | EXPR + EXPR | VAR [ EXPR ] | VAR ( EXPR )
NUM is a sequence of digits from the set, {0,1,2,...,9}.
VAR is a string beginning with a letter,
but not 'new', 'int', 'array', 'def', 'return', or 'end'.
TYPE ::= int | TYPE-array | TYPE1 -> TYPE2
===================================================
Now, think about C# or Java. These languages look a bit like the one above. 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 program for a propositional logic of data types. In the above program, variable x has type int (we write x: int), variable r has type int-array, and function f has type int -> int.
Here are the deduction laws for the above
language,
which prove propositions of the form, program-phrase: data-type.
(Read program-phrase: data-type as saying, ``program-phrase has
type data-type''.)
===================================================
decvar: -------------- v is a new decarray: --------------------- v is a new
new A v: A var name new A[n] v: A-array var name
+--------------------
| v2: A assumption
| ...
| e: B
+--------------------
def: ------------------------------- v1 and v2 are new var names
def v1(A v2) return e: A —> B
def v1(A v2) return e: A —> B e2: A
call: ----------------------------------------------------
v1(e2): B
v: A e: A
assign: ------------------
v = e: A
e1: int e2: int
num: ----------- add: ---------------------
n: int e1 + e2: int
new A v: A new A[n] v: A-array e: int
ref: ------------------ arrayref: -------------------------------------
v: A v: A-array
v: A-array e: int
index: ---------------------
v[e]: A
===================================================
A compiler uses the deduction rules to prove that a program is well-typed.
Here is the proof that the example program is well-typed:
1. new int x: int decvar
2. new int[4] r: int-array decarray
3. x: int ref 1
4. 0: int num
5. x = 0: int assign 3, 4
+------------------------------------
| 6. a: int assumption
| 7. 1: int num
| 8. a + 1: int add 6,7
+------------------------------------
9. def f(int a) : return a+1 end: int -> int def 6-8
10. 1: int num
11. x+1: int add 3,10
12. r: int-array arrayref 2
13. r[x+1]: int index 12, 11
14. r[x+1] = 1 assign 13, 10
15. f(x): int call 9,3
16. x = f(x): int assign 3, 15
This is how type checking works.
Here is your exercise:
Write a proof in the above style that shows this program is well-typed:
new int a;
a = 2;
new int[9] b;
b[a + a] = a;
def g(int-array c) return c[4] end;
a = g(b)