Clarification of (car 'atom) ?

[jdiamond]

In class, and in our notes, we have:
(consp x) = nil -> (car x) = nil

(and similarly for cdr.)

But in ACL, you will get an error if you pass an atom to car or cdr.
(The exception seems to be nil.)

I was wondering if you could clarify where this division occurs
between what ACL allows and the logic system we're building up in
class?

Thanks,
- Jeff

[Sandip Ray]

Hi,

[ I am copying Matt Kaufmann and J Moore, in case they have further
clarifying remarks to make in this issue. I know quite a few in
class have been stumped by this error. ]

In the logic it is indeed true that (car x) = nil if x is an atom.
And ACL2 will easily prove this as a theorem.

ACL2 !>(thm (implies (atom x) (equal (car x) nil)))

But we reduce the conjecture to T, by primitive type reasoning.

Q.E.D.

Summary
Form: ( THM ...)
Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

Proof succeeded.
ACL2 !>

However, when you _evaluate_ a ground term (that is, one which does
not contain free variables), ACL2, in its default mode, tries to do
the evaluation using the underlying Lisp. Using the underlying Lisp
enables ACL2 to evaluate a term fast. However, the use of Lisp for
evaluation means that attempting to evaluate (car 7) in ACL2 will
cause an error.

The error, however, does not have anything to do with the ACL2 logic,
just the evaluation in ACL2's default mode.

On the other hand, ACL2 has a mode in which you can evaluate a ground
term to give exactly the answer that the logic should give. To use
this mode, do the following:

ACL2 !>(set-guard-checking :none)

Turning off guard checking entirely. To allow execution in raw Lisp
for functions with guards other than T, while continuing to mask
guard violations, :SET-GUARD-CHECKING NIL. See :DOC
set-guard-checking.

ACL2 >(car 7)
NIL

Since we are currently interested in the _logic_, and not in
efficiency of evaluation, I think it is a good practice to type the
first form (set-guard-checking :none) at the beginning of your ACL2
session, that is, before attempting any evaluation. Then you'll see
evaluation of terms to produce results as you expect from the axioms.

ACL2 has an elaborate mechanism called "guards" tying the execution in
the logic to Lisp evaluation. We have not gotten into guards yet ---
we'll perhaps get into them some time later in the course when
evaluation efficiencies become a concern. But for now, my advice is
to ignore guards (which is what setting the guard-checking to :none
does). If someone is interested in guards and how they connect ACL2
with Lisp, I urge you to look up the topic guard at the ACL2
documentation (user's manual), which is available from the ACL2 Home
Page (http://www.cs.utexas.edu/users/moore/acl2).

Hope this provides some clarification.

Thanks,

-- Sandip

DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=googlegroups.com; s=beta;
h=domainkey-signature:received:received:x-sender:x-apparently-to
:mime-version:content-type:received:date:x-ip:user-agent
:x-http-useragent:message-id:subject:from:to:reply-to:sender
:precedence:x-google-loop:mailing-list:list-id:list-post:list-help
:list-unsubscribe:x-beenthere-env:x-beenthere;
bh=qRv/EPxfpAnbg3tAgugolwQU/FJQg0jdScV4wXqXSlw=;
b=omUDUsxxSfRFOa2IqEPHh5J5p7i2Iql4HVKGnP+OcEMEAbkk8k3RoIgFuHrc1Xu3Gv
w3MU/nQ0bIgisWbcykfAOpyrDlGT/ySqG/lno+hdDi0JyBX91PJjUA0nYflE22T7Io/Y
aOdM0K+K9YTqp6Adw+Bn0xA2ftZ59JZPAL7U4=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type:date:x-ip
:user-agent:x-http-useragent:message-id:subject:from:to:reply-to
:sender:precedence:x-google-loop:mailing-list:list-id:list-post
:list-help:list-unsubscribe:x-beenthere-env:x-beenthere;
b=Ew+Pb7MAYmaSmjtcOjgg8tBn/simkmg0988Rd2JH3fWRAvIuZdLISSfnWG3mCFo3z5
p0B98gYTFJ2Wk7cqF2y5+LJ/ZAgJ1jD06o1u2Cq1S9Tx/xjgt7gB1QQmUn7f6YZrbqix
k6IOVyk9DqJI3yQhMP0/kEuKtZQrA5GVKLsA4=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Thu, 18 Sep 2008 09:43:41 -0700 (PDT)
X-IP: 128.62.155.171
X-HTTP-UserAgent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; en-US; rv:1.9.0.1) Gecko/2008070206 Firefox/3.0.1,gzip(gfe),gzip(gfe)
From: jdiamond <jeffrey...@gmail.com>
Reply-To: utexas-cs38...@googlegroups.com
Sender: utexas-cs38...@googlegroups.com
X-Google-Loop: groups
Mailing-List: list utexas-cs38...@googlegroups.com;
contact utexas-cs389r-...@googlegroups.com
X-BeenThere-Env: utexas-cs38...@googlegroups.com
X-SpamAssassin-Status: No, hits=0.6 required=5.0
X-UTCS-Spam-Status: No, hits=-110 required=165