A Few Comments on HWK #1

[jdiamond]

I'm about half way through HWK #1, and there were some questions that
seemed to require material not found anywhere in the Moore notes or
the text book. After laboriously reverse engineering them from the
answers, I confirmed them in office hours. Since reverse engineering
isn't the point of the exercise, I thought I'd share the results.

The single largest issue was a specific notation I'll call the "cons
without parenthesis."

We all know that (a b) is a macro for (a . (b . nil)). Similarly, (a
(b . c)) would be a macro for (a . ( (b . c) . nil)).

But in the homework we see a syntax like this:

(a b c . d)

I initially assumed this meant (a b (c . d)), but it does not. Also
it is only legal as the last element of a list, e.g.
(a . b c d) is illegal. (a b . c d) is illegal.

I finally verified that this is an ad hoc syntax to specify the
rightmost leaf of a binary tree, and cannot be viewed as any form of
recursive definition.

So:
(a b c . d) = (a . (b . (c . d) ) )

And
(a b c) = (a b c . nil)

In retrospect, something like this is needed to harness the list
syntax for general binary trees.
=========================================
Now for some more trivial points:

From the homework answers we see that a number is NOT a constant
unless it is quoted. Whereas the text book says it is, and later in
the notes, they say that a number without a quote is an abbreviation
for one with a quote.

The homework also implies that '(1 2 3) is NOT a constant, but the
textbook says it is. I assume there are subtleties here. Later in
the notes it speaks of an expansion of '(1 2 3). Seems like this is
just an issue of macros vs final forms...

Lastly, the textbook says 12E-7 is NOT a symbol, but here I'm pretty
sure the text book is wrong and it is.

The second half of the homework looks pretty straightforward... Once
you parse through the math...
- Jeff

[jdiamond]

Just to punctuate the trivial point about quoted numbers:

In the homework, we see things like this:
(cons (cons ’1 ’2) (cons (cons ’3 ’4) ’nil))

Well, in both Common LISP AND ACL2, this produces an error until you
remove all the quotes:
(cons (cons 1 2) (cons (cons 3 4) nil))

So it seems like not only is quoting a constant redundant, it's
actually an error...

[Sandip Ray]

Hi,

If you do this:

(cons (cons '1 '2) (cons (cons '3 '4) 'nil))

then you'll see that the value is ((1 . 2) (3 . 4)). So quoting
should be fine. Indeed, if you care, in the logic the term is '1 and
its value is the number 1. So, for example the term is (cons '1
'2). Except, as a convenience, ACL2 lets us write (cons 1 2).

Let me know if you have further questions.

-- 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:content-transfer-encoding:received:date
:in-reply-to:x-ip:references: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=n+rg12nSQf4jDHMNyXBvDNi3OgrM4uSEArpLdU4sLQE=;
b=WV86O439QH2pvBk5an/vTJq01RJGgS8dLyyLgqoeptb3YHjnjYbKA29bgps2Tp3dk8
iU126SNHx9qYAvaUNdBWVMkSj/O335iD+8Ec0DZqTHp+r1EZ0gXqYRMbxwz6PPsBLJAS
fxQJ+RL6dk+cCtegSWQn9dqRuAd2IlyIHdYe0=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type
:content-transfer-encoding:date:in-reply-to:x-ip:references
: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=kImuqLPLkyWYl8iIIurDHdFp+gWiTgCEiEZRxOH6NwR2MHw/Q56BJIK37GeHJDZnFl
NLgLAXQzr1ZFr2Xv3HfvYcMWJrnMMz64JfzqdP9WAQSKyKk5uruPq74QeIvqfmtH48jQ
hEa7+mINQpbVhNs+GDeM2+bb3xL3m5Oj6OMcs=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Tue, 2 Sep 2008 18:31:05 -0700 (PDT)
X-IP: 128.62.161.131
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=-130 required=165

[jdiamond]

I solved the quoting issue. It's not true that redundant quotes are
illegal - they do in fact work.

What I had forgotten is that in making the text file for my homework I
had copied the homework problems directly from Moore's notes into my
text file. Although I still had a text file and everything looked OK,
for some reason the quotes got copied through as a different ASCII
code than the conventional quotes. I used a lot of cut and paste to
prevent errors, and since my original source of the quotes was this
text file, all my quotes got corrupted.

So LISP and ACL2 rejected the quotes because they were some foreign
character version of a quote.
When I hand typed them from scratch, everything worked fine.

Sorry for all the confusion. I guess the empirical approach to
learning can have some pitfalls as well. :)

- Jeff