Child pages
  • CSU 290 (Spring 2008)

Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 5.3

...

What you should do right now: Make sure you are logged into the wiki. (Select "Log In" under "Your Account" below if not, use you CCIS credentials to log in.) Look at the bottom of the page, under "Other Features", top right icon is an envelope. Press that button. That will register you as watching this page. Basically, every time the page changes, you get an email saying so. Keeps you from having to check the page regularly.

...

February 15: Formal

...

Proof for ~(t=nil)

Here is a complete formal proof for ~(t=nil) using the axioms I gave in class. (This is the proof that I started on Monday, but ran out of time 5 steps into the proof.)

...

Decision Procedure for Equivalences

Coming soonThis decision procedure is used to establish whether an implication where the hypotheses are equalities and the conclusion is also an equality is true, in the special case where this information can be decided without relying on the definition of the functions in the expression. (For instance, this may be interesting when we have no definition for the functions in the expression; that's what defstub does, by the way, it "defines" a function without actually giving an actual definition.)

Let's be more concrete. Suppose that we have no information about functions f and g, but we are asked to prove that:

No Format

(implies (and (= a c)
              (= (f a) b)
              (= (g c) c)
         (= (f (g a)) b))

Here's an argument that us humans can come up with easily, written in infix notation to simplify the presentation:

No Format

(f (g c)) = (f (g a))  # because a = c
          = (f c)      # because (g c) = c
          = (f a)      # because a = c
          = b          # because (f a) = b

No problem. How does ACL2s prove it, though? It uses a procedure called congruence closure. It has the advantage of working for an arbitrary equivalence relation, not just equality.

You can find precise definitions of the congruence closure algorithm in many places. See these slides on congruence closure if you are curious. I will describe it at a very high level here.

First off, take the formula you have, and extract all the subterms in it. The subterms are all the function applications that occur in the expression, and all the constants. List them all, the order is not important. Here are the subterms in the example above, listed in roughly in order of increasing complexity:

No Format

a  
b  
c  
(f a)  
(g c)  
(g a)  
(f (g a))

Note that (g a) is a subterm because it appears in (f (g a)).

Good. Now, the procedure is to repeatedly look at the equations in the hypotheses (there are three in our example), and "lump" together the terms in our list that the equation force to be equal. Lumping terms together may lead to further lumping, because new things may be made equal that we didn't know before were equal.

Let's start. Let's look at the first equation a = c. It tells you to lump together a and c. Let's do that:

No Format

a  c  
b  
(f a)  
(g c)  
(g a)  
(f (g a))

I am representing lumps by putting terms on the same line. Terms lumped together are simply terms that can be proved to be equal using the equations we have been looking at. Knowing that a and c are equal tells you also that (g a) and (g c) are equal, so we can lump those two together too:

No Format

a  c  
b  
(f a)  
(g c)  (g a)  
(f (g a))

That's it, we cannot lump things together any further based on what we know.

Let's look at the second equation, (f a) = b. It tells you to lump together (f a) and b. Easy enough:

No Format

a  c  
b  (f a)  
(g c)  (g a)  
(f (g a))

That's it, we cannot lump things together any further.

Let's look at the last equation, (g c) = c. It tells you to lump together (g c) and c. Now, because c is already lumped with something, and (g c) is also already lumped with something, let's merge the respective lumps. (After all, lumping just means that things can be proved equal.)

No Format

a  c  (g c)  (g a)  
b  (f a)  
(f (g a))

Oh, now we've learned a lot, in particular, that (g a) = a. This means that (f (g a)) = (f a), so that we can lump (f a) and (f (g a)) together:

No Format

a  c  (g c)  (g a)  
b  (f a)  (f (g a))

And that's it, we cannot lump things any further. And we've exhausted all of our equations in the hypotheses. So the lumps above represent all the different things that can be proved equal to each other. Our conjecture asks whether the three equations imply that (f (g a)) = b; in other words, do the three equations ensure that (f (g a)) and b are lumped together by the above procedure? It is easy to see that yes, they are. Therefore, the algorithm (and ACL2s) will report that the conjecture is true.

...

April 21: Study Guide

As requested by a few students, here is a quick study guide for the final. (There is nothing here that has not been said already in class.) As we mentioned in class, the final will be a cross-section of all the tests we have had during the semester. Roughly, there should be one question per exam.

So what did those tests cover?

Test 1:

  1. the basics of the ACL2 programming language
  2. total functions,
  3. the use of the design recipe to develop functions

Test 2:

  1. lists and true lists
  2. quotation
  3. design recipe for recursive functions over true lists

Test 3:

  1. Boolean logic
  2. proving theorems using equational reasoning
  3. falsifying conjectures

Test 4:

  1. the induction principle (give proof obligations)
  2. proving proof obligations

Test 5:

  1. more difficult inductions (idenfitication of lemmas)
  2. generalization
  3. using different substitutions in the inductive proof obligation

Test 6:

  1. The ACL2s theorem prover and the waterfall model
  2. rewriting
  3. understanding proof reports, including identifying interesting checkpoints
  4. decision procedures for Boolean logic and congruence closure