Can a symbol like 'two evaluate to an assigned value?

[jdiamond]

That was my question.

The answer was no. A VARIABLE symbol two (without the quote) can
indeed be assigned a value like 2. But just as '2 evaluates to the
symbol 2, 'two evaluates to the symbol two.

Implication: (equal '2 'two) will always return 'nil

[jdiamond]

As an aside here, note that both constants and variables are both
thought of as constants, i.e., we are really discussing quoted
constants and variable constants. When a variable constant is
assigned a value (at the top level), it's marked with asterisks, e.g.
*PI* evaluates to 3.14159.... But when a function argument list is
defined, they are acting more like variables than constants.

So what if you try to put a variable in a quoted list, such as '(1 2
*PI*) ? It won't work - the *PI* is then interpreted as a quoted
constant and not a variable constant.

Anyone feel free to comment on these kinds of things. I'm trying to
get all the subtleties down.

[jdiamond]

OK, I was a little off on terminology since we haven't been taught
everything yet. But the textbook says something like *PI* has been
explicitly assigned a value using defconst, and that this is a
constant symbol distinct form a variable symbol.

[Sandip Ray]

Hi,

I thought I'd add a few things.

In a certain sense you cannot write '(1 2 *PI*) as a term and think of
*PI* as a variable symbol.

To recap what we said in class:

A term is (1) a variable symbol
(2) a quoted constant
(3) something of the form (f t1 t2 .... tn) where f is a
function symbol of arity n and t1 ... tn are terms.
Nothing else is a term.

Since you write '(1 2 *PI*) as a term, you must be writing a quoted
constant. That is, you are using rule 2. But then you are not
writing a variable.

We tend not to talk about "variable constants" in the logic. We talk
about objects in the universe, and their representations as terms. A
quoted constant is simply any object in the universe with a quote in
front of it.

> When a variable constant is assigned a value (at the top level),
> it's marked with asterisks, e.g. *PI* evaluates to 3.14159....

I am presuming you mean the construct defconst in ACL2. I'll try to
talk about this in class in the coming week (have not gotten to it
yet), but such things *logically* are best seen as 0-ary functions.
(This actually happens to be a macro, but we'll deal with that.)

BTW, just a little bit of logical nit-picking here for the ACL2 logic:
the object 3.14159... is *not* an object in the ACL2 universe (since
we do not have decimal representation in the ACL2 logic), so no term
can evaluate to this object. Something can of course evaluate to the
fractional representation of this object.

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: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=k6ZQTUREA8CDMP03j7fQV//rvnxWKMZ/jpcY/TZ4uHA=;
b=lh6EFUPOBoVIQWXTfzbTGg+yZhag4+l0fcAOTtY8lN9/ebHww8FqAqJTt/xX8z37l9
sxFOvoSHmUK+EkkaMxKxYVp3j1Bg0wOSr3rem70DkBq2twYPl3KOZK/psQ6emeIQaAoA
0LaZwrPWBx0Lmco9OFDQdZ7XOKq9lfQsbccFs=
DomainKey-Signature: a=rsa-sha1; c=nofws;
d=googlegroups.com; s=beta;
h=x-sender:x-apparently-to:mime-version:content-type: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=FclK14YrqeYKERD9H4qNkGKwju81gRoF78Xpvm0SlwMFhGlSm3/tWIsld/5iULBPrz
ZGUQ249/v2TQ/jXnEzxyezayalZV2RvBuDuIo88nBiDY3PVoGzPfXQBnxccYQBJyc/hS
R4slcYCh8KTpLzUSlYZosvwl4aEPBcdI04epM=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Thu, 4 Sep 2008 17:48:27 -0700 (PDT)
X-IP: 128.62.214.150
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