Due Monday, 19 Feb @ 5:00 pm
This is an ACL2 assignment. You need not turn in handwritten proofs. However, you may find that writing them by hand helps you to guide ACL2.
Design an insertion sort program for lists of numbers. Prove it correct. A sorting program is correct if it meets two conditions:
It always produces an ordered list.
It always yields a permutation of its input.
You will need to write functions that specify what it means to be an ordered list and what it means for two lists to be permutations of each other.
Consider a small language of arithmetic expressions that has numbers, variables, addition, and multiplication:
AE ::= Number | Symbol | (add AE AE) | (mul AE AE)Environment = List[(cons Symbol Number)]
Design a program that consumes an AE and an environment and produces the numeric value of the expression.
Programming language implementations often perform transformations on programs to make them run faster. One such transformation is called constant-folding. A constant folder consumes an arithmetic expression and produces an arithmetic expression where the constant subexpressions are already simplified. For example:
(constant-fold (add 'x (mul 3 5))) = (add 'x 15)(constant-fold (add 4 3)) = 7(constant-fold (mul (add 4 (mul 3 2)) 'z) = (mul 10 'z)(constant-fold (mul (add 'x 'y) 42)) = (mul (add 'x 'y) 42)
Write a constant folder for AE's, and prove it correct. A program transformation is correct when the transformed program behaves the same as the original.
We discussed a simple proof language like the Fitch system that you use in your Symbolic Logic course. The syntax is:
P ::= A | P -> P | P /\ P
A ::= <Symbol>
D ::= (assume P D) | (modus-ponens D D)
| (both D D) | (and-left D) | (and-right D)
| P
Write the program simplify : D List[P] -> Maybe[P]* that produces the proposition that a given deduction D proves, if any. If the deduction is erroneous, produce nil.
*Define Maybe[X] = (union X {nil}).