Developers-guide-logic
Logical Considerations
This Developer's Guide may give the impression that ACL2
maintenance is primarily a programming exercise, and that is probably true.
However, there are some subtle logical
considerations that need to be considered when working with some parts
of the implementation. This topic addresses an assortment of such
considerations, often by pointing to source code comments. Additional reading
for those intrigued by logic is the paper: ``Structured Theory Development for
a Mechanized Logic,'' Matt Kaufmann and J Strother Moore, Journal of Automated
Reasoning 26, no. 2 (2001), pp. 161--203.
Note: The examples below are by no means
comprehensive! You are encouraged to extend this documentation topic
with additional logical considerations as they arise. Also see the Essay on
Soundness Threats.
Histories, chronologies, and theories
An ACL2 session has at least three logical interpretations, as follows.
- The corresponding history, which is
the sequence of all axiomatic events from the session: this
includes defun, defchoose, and defaxiom events, as
well as encapsulate events with non-empty signatures. It does
not include defthm events.
- The corresponding chronology, which is
the sequence of all events from the session with logical content. Thus the
history is a subsequence of the chronology, but the chronology also includes
defthm events.
- The corresponding theory of the
session, which is the first-order theory of its history, that is, axiomatized
by the formulas in its history. (Careful: This theory is not sensitive to
which runes are enabled, unlike the macro, current-theory.) A basic
property of ACL2 is that all formulas in the session's chronology are provable
in the session's theory. In particular, by restricting to the chronology of
events up to and including a given defthm event, we see that the formula
of that event is provable from the axiomatic events that precede it.
When a session S1 is extended to a session S2 without using
defaxiom events, then the theory T2 for S2 is a conservative
extension of the theory T1 for S1: that is, every theorem of
T2 whose function symbols all occur in T1 — that is, are all
introduced in S1 — is a theorem of T1. An important corollary
is that if a session has no defaxiom events, then its theory is
consistent.
Note that defattach events are ignored for all three notions listed
above. There is also a notion of evaluation theory, which is the
extension of the session's theory by the equations that equate each function
with its attachment. A basic property is that every evaluation theory built
from a session free of defaxiom events is the theory of some history that
is free of defaxiom events, and thus (by the corollary stated in the
preceding paragraph) is consistent. For a detailed development of theory
supporting the use of defattach (though this can probably ignored unless
you are doing deep work with defattach), see the source code comment,
``Essay on Defattach.''
There is also a logical explanation for apply$, which is based on
the notion of evaluation theory mentioned above for defattach. The
upshot is that a certain construction, the ``doppelganger construction'',
produces an evaluation theory in which every warrant is valid. For
detailed theoretical justification (probably not necessary for most
developers, unless perhaps they are doing deep modifications pertaining to
defattach or apply$), see the source code comment, ``Essay on
Admitting a Model for Apply$ and the Functions that Use It.''
IN THIS SECTION WE CAN FOCUS MAINLY ON THE DISPLAYS.
Many soundness bugs in past versions of ACL2 — indeed, perhaps the
majority of them — can be attributed to a subtle mishandling of local events. Perhaps the only advice possible in this regard is the
following: Think carefully about the effects of local when making
event-level changes to ACL2!
Consider for example the following, seemingly innocuous ``enhancement'':
allow verify-guards to comprehend macro-aliases (see macro-aliases-table). Such an ``enhancement'' would be unsound! Instead, a
similar but sound enhancement, verify-guards+, was introduced (into
Version 6.3). See verify-guards+ for an example,
using encapsulate and local, for why such an enhancement to
verify-guards would be unsound.
We turn now to discuss a key mechanism for avoiding potential soundness
issues caused by local: the ACL2-defaults-table. Because of the
logical information stored in this table, it is prohibited to modify
this table locally, as we illustrate with a couple of examples. First
consider the following introduction of a program-mode function, f,
that clearly is inadmissible in logic-mode.
(encapsulate
()
(program)
(defun f () (not (f))))
If the (program) event were allowed to be local, then the second pass
of the encapsulate event would introduce f in logic-mode, creating
an inconsistent theory!
A slightly more subtle example is the following.
(encapsulate
()
(set-ruler-extenders :all)
(defun foo (x)
(cons (if (consp x) (foo (cdr x)) x)
3)))
The induction scheme stored for foo is as follows, which is the same
as would be stored for the simpler definition, (defun foo (x) (if (consp
x) (foo (cdr x)) x)). (Don't worry about the form of the structure below.
Further relevant discussion may be found below in the section, ``Induction,
recursion, and termination.'')
ACL2 !>(getpropc 'foo 'induction-machine)
((TESTS-AND-CALLS ((CONSP X))
(FOO (CDR X)))
(TESTS-AND-CALLS ((NOT (CONSP X)))))
ACL2 !>
The 'induction-machine property is computed based on the
ruler-extenders. So if the event (set-ruler-extenders :all) above could
be made local, we would be storing the same induction machine as for the
following definition.
(skip-proofs
(defun foo (x)
(declare (xargs :measure (acl2-count x)))
(cons (if (consp x) (foo (cdr x)) x)
3)))
But that induction-machine is unsound!
(thm nil :hints (("Goal" :induct (foo x))))
The two examples above illustrate the importance of thinking about whether
an event can soundly be local. If not, then it may be best for that event to
be one that sets the ACL2-defaults-table, like program and
set-ruler-extenders, since table events that set the
acl2-defaults-table are not permitted to be local.
IN THE WORKSHOP THE FOCUS WILL BE ONLY ON THE LOGICAL DIFFERENCE.
There is a fundamental logical difference between wrapping skip-proofs around a defthm event and using defaxiom. When
using skip-proofs, the user is promising that the ensuing proof
obligations are indeed theorems of the theory of the current ACL2 session.
However, the meaning of defaxiom is to extend that theory with a new
axiom, one which is generally not provable from the session's theory. See
skip-proofs and see defaxiom. This logical distinction has
ramifications for the implementation, as we now describe.
Since the use of skip-proofs carries an implicit promise of
provability, the implementation can largely ignore the question of whether an
event was, or was not, introduced using skip-proofs. The key reason to
do any such tracking is to inform certify-book when the use of keyword
argument :skip-proofs-okp t is required.
On the other hand, it is critical for soundness to track the use of defaxiom. In particular, it is unsound to allow local defaxiom
events. That is obvious from the following example, which would leave us in
an ACL2 world in which nil is provable even though there is no
defaxiom event in that world.
(encapsulate
()
(local (defaxiom bad-axiom nil :rule-classes nil))
(defthm bad-theorem nil
:hints (("Goal" :use bad-axiom))
:rule-classes nil))
That event is, of course, rejected by ACL2. The following, on the other
hand, is accepted; but this does not demonstrate unsoundness of ACL2, because
the user violated the implied promise that, quoting from above, ``the ensuing
proof obligations are indeed theorems of the theory of the current ACL2
session.''
(encapsulate
()
(local (skip-proofs (defthm bad-axiom nil :rule-classes nil)))
(defthm bad-theorem nil
:hints (("Goal" :use bad-axiom))
:rule-classes nil))
We conclude this section by noting that there are different ``levels'' of
skip-proofs used by the implementation that are not directly visible to
the user. The basic skip-proofs you see around an event generates a
binding of state global 'ld-skip-proofsp to t. However, when you
include a book, state global 'ld-skip-proofsp is bound to
'include-book, which has two major effects: local events are
skipped, and some checks are omitted. For example, the redundancy checks
normally performed after (set-enforce-redundancy t) are, as one would
hope, omitted when including a book. If you tags-search the sources for
``(enforce-redundancy'', you'll see that it is used to implement
events (see for example the definition of defconst-fn); then if you look
at the definition of enforce-redundancy, you'll see that its check is
skipped when state global 'ld-skip-proofsp is bound to
'include-book, hence when a book is being included. Also see ld-skip-proofsp.
Induction, recursion, and termination
Every proposed definition with recursion generates two related artifacts: a
proof obligation that is generally described as the termination proof
obligation, and an induction scheme to be stored if the definition is
admitted. A key soundness requirement is that the
termination proof obligation justifies use of the induction scheme.
This produces a tension, as can be seen by the analysis below of the following
example.
(defun f (x)
(if (consp x)
(cons (if (consp (car x)) (f (car x)) x)
x)
x))
The generated induction is displayed symbolically just below: when proving
a proposition (P x), the induction step is to assume (consp x) and
(P (car x)) when proving (P x), and the base case is to assume
(not (consp x)) when proving (P x).
ACL2 !>(getpropc 'f 'induction-machine)
((TESTS-AND-CALLS ((CONSP X))
(F (CAR X)))
(TESTS-AND-CALLS ((NOT (CONSP X)))))
ACL2 !>
There is a comment just above the defrec for tests-and-calls that
explains that record structure. The corresponding termination
scheme may be seen by evaluating (trace$ termination-machine) before
submitting the defun form above. Here is the result.
<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X))
(F (CAR X)))))
What this means is that ACL2 must prove that under the hypothesis (consp
x), then (acl2-count (car x)) is smaller than (acl2-count x).
That proof obligation clearly justifies the induction scheme described
above.
But let us try an experiment in which ACL2 is instructed to consider, for
termination and induction, any IF-tests that are not at the top level
— in this case, within the call of cons. In a fresh session, we
try this instead.
(defun f (x)
(declare (xargs :ruler-extenders (cons)))
(if (consp x)
(cons (if (consp (car x)) (f (car x)) x)
x)
x))
The induction machine produced this time includes the extra if test or
its negation. It says that when proving a proposition (P x), the
induction step is to assume (consp x), (consp (car x)), and
(P (car x)) when proving (P x); one base case is to assume (consp
x) and (not (consp (car x))) when proving (P x); and the other
base case is to assume (not (consp x)) when proving (P x).
ACL2 !>(getpropc 'f 'induction-machine)
((TESTS-AND-CALLS ((CONSP X) (CONSP (CAR X)))
(F (CAR X)))
(TESTS-AND-CALLS ((CONSP X) (NOT (CONSP (CAR X)))))
(TESTS-AND-CALLS ((NOT (CONSP X)))))
ACL2 !>
This time there is a different termination proof obligation as well,
stating that (car x) has a smaller acl2-count than that of x
under the conjunction of the pair of assumptions (consp x) and
(consp (car x)). As before, it justifies the induction scheme just
above.
<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X) (CONSP (CAR X)))
(F (CAR X)))))
Now suppose that the implementation is careless, by making the ruler-extenders affect the termination proof obligations but not the
induction scheme. Consider the following example.
(defun g (x)
(declare (xargs :ruler-extenders (cons)))
(cons (if (consp x) (g (car x)) x)
x))
This produces the termination proof obligation represented as follows
(again from a trace), which says that assuming (consp x), (acl2-count
(car x)) is less than (acl2-count x). Note that this is indeed a
theorem.
<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X))
(G (CAR X)))))
To see what the induction scheme would be if we ignored the
ruler-extenders, we submit the following.
(skip-proofs
(defun g (x)
(declare (xargs :measure (acl2-count x)))
(cons (if (consp (car x)) (g (car x)) x)
x)))
The corresponding induction machine states that to prove (P x), we may
assume (P (car x)).
ACL2 !>(getpropc 'g 'induction-machine)
((TESTS-AND-CALLS NIL (G (CAR X))))
ACL2 !>
If we let (P x) be (consp x), then clearly this induction scheme
allows us to prove (consp x) for all x!
(thm (consp x)
:hints (("Goal" :induct (g x))))
This induction scheme is thus clearly unsound.
The moral of the story is this: As the termination machine is modified to
accommodate the ruler-extenders, the induction machine must be modified
accordingly. More generally, and as already noted: The termination machine
must justify the induction machine.
Other tricky stuff
The logical underpinnings of ACL2 can be a bit overwhelming when considered
together, so the following paragraphs should be taken as a suggestion for what
to explore only when you're in the mood for some logic, and also as an
acknowledgment that many subtle logical issues exist. It is NOT meant
as a prescription for what you need to explore! Moreover, it is far from
complete.
The foundations of metatheoretic reasoning can be challenging. If you
tags-search for ``; Essay on Metafunction Support'', you'll see two relevant
essays. But a much longer essay is the ``Essay on Correctness of Meta
Reasoning''. That essay even ties into the ``Essay on Defattach'', at the
mention of the Attachment Restriction Lemma. If you decide to change the
handling of metafunctions or clause-processors or their corresponding rule-classes, :meta and :clause-processor, other than fixing coding
bugs or making extra-logical changes such as output, you probably should read
these Essays. Of course, before reading these or any essays, it is generally
a good idea to read relevant user-level documentation, such as the
documentation for meta or clause-processor.
A few other features of ACL2 with interesting logical foundations are
defchoose, defabsstobj, and the interaction of packages with
local (see the ``Essay on Hidden Packages'').
NEXT SECTION: developers-guide-programming
