Good form when designing functions on lists...

[jdiamond]

It seems that normal list operations never copy the objects the tree
points to. However, it seems like it is good form for us to make sure
that we completely copy the nodes themselves when writing a list
function.

On the one hand, this is pretty inefficient. For example, if we want
to append one list to another, we only need to change a single
pointer. But on the other hand, the consequences could be disastrous
if the nodes aren't all copied. For example, if the list that has
been appended is then altered, that alteration will also appear in the
appended list.

So I'm guessing we're supposed to ignore the cost and copy all the
pointer nodes?
- Jeff

[Sandip Ray]

Hi Jeff,

You're right. Since the logic is applicative there is no destructive
updates (at least for now). So if we append two lists together, we
must create a third list which will be produced through copying nodes
from one list to another.

At this point we're not concerned about the *efficiency* of such
functions. But the logic of ACL2 actually supports several efficiency
features (including destructive updates). We will learn about
efficiency in an applicative setting hopefully later in the class.

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=ZtiEy2k2/BnXrEDe6ZgLCWMDfKFbsNIw/te0sda5NeA=;
b=sVnYEVDzDPzGRpu6ZrR2kQHTJk2IhSLbbBMSDpAz+nr6BjDhs+CrSdqNVNJiKvVwz0
mY/kRf1rVyPrpEnaye6f3zs95cUX0hI6mAG5UOjOms33YK5zibPTekEF9JZRdD44jUOm
wSK0XlBMYC1sWxbHnw2G2++O7CfGSb0+qh8Cc=
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=X3dLwH4IOKl+ezCqOOxK0KFs4dLK2rIijwEEouF+0rcHNFQCZsyF8UDWLnn4DeG9qb
xYF4epPKJTGA/BLYcJKm5v5TyIEQmw2oxUUUZePf5QqiobtgM0YtFbZhIvulthlOy8h7
99nBMT4SDGk+n8UldhMOvsF75QE00ZT/eGl9w=
X-Sender: jeffrey...@gmail.com
X-Apparently-To: utexas-cs38...@googlegroups.com
Date: Thu, 11 Sep 2008 17:20:24 -0700 (PDT)
X-IP: 128.62.148.167
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