From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: Noah Lavine Newsgroups: gmane.lisp.guile.devel Subject: Re: Avoiding variable clashes Date: Wed, 13 Apr 2011 21:08:21 -0400 Message-ID: References: <6388D072-D554-4C60-AAAE-9E3E9CB8E54D@telia.com> <8709414F-2FA6-409C-840A-E2BED1CE4F3F@telia.com> NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1302743313 22013 80.91.229.12 (14 Apr 2011 01:08:33 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 14 Apr 2011 01:08:33 +0000 (UTC) Cc: Andy Wingo , guile-devel To: Hans Aberg Original-X-From: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Thu Apr 14 03:08:27 2011 Return-path: Envelope-to: guile-devel@m.gmane.org Original-Received: from lists.gnu.org ([140.186.70.17]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1QAB2p-0005tG-4d for guile-devel@m.gmane.org; Thu, 14 Apr 2011 03:08:27 +0200 Original-Received: from localhost ([::1]:53271 helo=lists2.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QAB2o-0007hL-K6 for guile-devel@m.gmane.org; Wed, 13 Apr 2011 21:08:26 -0400 Original-Received: from eggs.gnu.org ([140.186.70.92]:43554) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QAB2l-0007h5-4C for guile-devel@gnu.org; Wed, 13 Apr 2011 21:08:24 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1QAB2k-0006j8-8x for guile-devel@gnu.org; Wed, 13 Apr 2011 21:08:23 -0400 Original-Received: from mail-vx0-f169.google.com ([209.85.220.169]:43658) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1QAB2k-0006j4-5z for guile-devel@gnu.org; Wed, 13 Apr 2011 21:08:22 -0400 Original-Received: by vxk20 with SMTP id 20so1250491vxk.0 for ; Wed, 13 Apr 2011 18:08:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; bh=2DQmiG0FfAUD+Snhp9pwDEL/zdm4q6XKwJlomKs2SbA=; b=ib52Kpligki47T5a2+xSZkbD0wTbssIeFTOy/ybZjrOb7X0UeGmkZZx7EjM1Fa+w8/ +gMCKYlZyUTMRjCS1cuySdXzWZ90zEiECjxbdzNYn3q+YKmxRkjl9C0Fm2YSE71g9fiy FlHcY/Dd7CjsXgjyn+yMOC5C++YgFYnsX6VDY= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=VdL3s3+c0IEtw+VRhSdYKK9/1eQ2uMLKHYK789hFPA1bseHQRqm/VZoNonbbqcTWjS J+m/Ju5YI+/dObZeYjHmeq+yy7uUtlFjwgYwQEv0ygMmHlPpZynRptCSw4yy2gG748xB gKpIIA+6ECA6OmIbDcvI3tJ5ZEmxb+juVR6HA= Original-Received: by 10.52.99.198 with SMTP id es6mr199585vdb.201.1302743301808; Wed, 13 Apr 2011 18:08:21 -0700 (PDT) Original-Received: by 10.52.166.233 with HTTP; Wed, 13 Apr 2011 18:08:21 -0700 (PDT) In-Reply-To: <8709414F-2FA6-409C-840A-E2BED1CE4F3F@telia.com> X-Google-Sender-Auth: Xuilxv8irojsIWVCiu34sy9OrUU X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.6 (newer, 2) X-Received-From: 209.85.220.169 X-BeenThere: guile-devel@gnu.org X-Mailman-Version: 2.1.14 Precedence: list List-Id: "Developers list for Guile, the GNU extensibility library" List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Original-Sender: guile-devel-bounces+guile-devel=m.gmane.org@gnu.org Xref: news.gmane.org gmane.lisp.guile.devel:12254 Archived-At: > The beta rule is in denotational semantics something like > =A0((lambda x . E_1) E_2) =3D> [E_2/x]E_1, E_2 free for x in in E_1 > where [E_2/x]E_1 means substituting all free occurrences of x with E_2. > > In addition, one has the alpha rule > =A0(lambda x . E) =3D> (lambda y . [y/x]E), y free for x in E > > Now, if one would want to implement say a quantifier 'forall', one would = still need the alpha rule, and substitution, but instead of the beta rule h= ave > =A0(forall x . E) =3D> [t/x]E, t free for x in E > where t is any term. One would have to write additional stuff to manipula= te it. But the alpha rule is tricky to implement. > > The generalization would be to admit defining operators b satisfying the = alpha rule > =A0(b x . E) =3D> (b y . [y/x]E), y free for x in E > where one can add additional evaluation rules. I believe you can implement all of that with the mechanisms of environments and gensyms. However, let me give a slightly different perspective on it, which is how I have come to think of these things: First, the alpha rule: the expressions (lambda (x) (+ x 1)) and (lambda (y) (+ y 1)) are equivalent by the alpha rule, because we have merely changed the name of a thing. The environment perspective is that you shouldn't think of 'x and 'y as variables at all. Instead, think that in the first expression the symbol 'x refers to some ideal "variable" object, which represents one "slot" where a value can exist. In the second expression, 'y refers to the same sort of object. Every different slot that can be referred to has a different one of these variable objects, so substituting one for another is pointless - there will never be a name conflict. For instance, the following expression has two "variable" objects, even though there is only one symbol naming them: (lambda (x) (lambda (x) (+ x 1))) We use environments to essentially replace symbols by the appropriate "variable" objects as soon as we see the symbols, so the rest of the compiler code never has to worry about one symbol naming two different things, or other weird cases like that. The fact that we represent different variables as gensyms is an implementation detail, and unimportant. (In fact, I might like to change that detail at some point to get better error messages, but it's not high on my to-do list.) Does this make sense to you? Noah