|
Computer Science 598A
Automated Theorem Proving
Andrew Appel
|
Spring 2003
|
General Information | Schedule | Assignments | Announcements
Assignment 10
The goal is to write a program in Twelf that can produce safety proofs for programs
that use lists, such as the reverse program in
list.elf:
reverse =
q gets zero ;
while (neq p zero)
(h gets_head p ;
p gets_tail p ;
q gets cons h q).
reverse_thm = triple (is_list @ p) reverse (is_list @ q).
In this assignment, you will accomplish some preliminaries;
the next assignment will complete the prover.
0. Setup
You should turn in one file, types.elf, that contains
all your work. This file should load in the context of
the as5/hoare/sources.cfg configuration.
The last part of your file should be the
Twelf queries. You don't need to show the results of running
the queries; I will run them myself.
1. Definition of type predicates.
A "programming language type" is defined by this kind of predicate in the
object logic:
ty : tp = num arrow form.
Define each of the following predicates:
is_list: tm ty = (already defined...)
is_cons: tm ty = (is a cons cell, not necessarily a list) ...
is_list_cons: tm ty = (is a list, and is not nil) ...
is_zero: tm ty = ...
2. Proofs of intro/elim lemmas
Prove these lemmas:
is_list_i1: pf (is_list @ zero) =
is_list_i2: pf (is_int @ X) -> pf (is_list @ Y) -> pf (is_list @ cons X Y) =
is_list_e: pf (is_list @ A) ->
pf (eq A zero or
exists2 [x][y] is_int @ x and is_list @ y and eq A (cons x y)) =
is_list_cons_e1: pf (is_list_cons @ A) -> pf (is_cons @ A) =
is_list_cons_e2: pf (is_list_cons @ (cons X Y)) -> pf (is_int @ X) =
is_list_cons_e3: pf (is_list_cons @ (cons X Y)) -> pf (is_list @ Y) =
3. Logic program for type union
Write a logic program that is given two types X and Y, and finds
the greatest lower bound, that is, the "best" type Z such that
(X is a subtype of Z) and (Y is a subtype of Z). Your program
should be invoked as follows:
t1 : tm ty = ...
t2 : tm ty = ...
%query 1 * P : find_union t1 t2 Z.
4. Semantic model of find_union
Restate your declaration of find_union as a definition:
find_union: ... = ... .
and prove each clause of your logic program as a lemma.
5. Logic program for combining type lists
Write a logic program combine that takes two lists
of typings A and B and produces the strongest list of typings that
is implied by A and also implied by B.
A "list of typings" is a right-associative
sequence of conjunctions, terminated by true.
Example:
v: tm num.
w: tm num.
x: tm num.
%query * 1 combine (is_list @ v and is_list_cons @ w and true)
(is_zero @ w and is_int @ v and is_list @ x and true)
C.
---------- Solution 1 ----------
C = is_list @ w and true.
____________________________________________
Don't write a semantic model of combine just yet.
6. Demonstration of find_union and combine
Demonstrate your logic program by running some sample queries.