From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5119 Path: news.gmane.org!not-for-mail From: Greg Meredith Newsgroups: gmane.science.mathematics.categories Subject: Re: typed lambda calculus:cartesian closed :sorted pi calculus:? Date: Sat, 29 Aug 2009 10:52:11 -0700 Message-ID: Reply-To: Greg Meredith NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-7 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1251724330 17680 80.91.229.12 (31 Aug 2009 13:12:10 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 31 Aug 2009 13:12:10 +0000 (UTC) To: Mike Stay , Categories Original-X-From: categories@mta.ca Mon Aug 31 15:12:03 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1Mi6fq-00015R-Gp for gsmc-categories@m.gmane.org; Mon, 31 Aug 2009 15:11:54 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1Mi66p-0005hU-Ff for categories-list@mta.ca; Mon, 31 Aug 2009 09:35:43 -0300 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5119 Archived-At: Dear Mike, i missed another point in your mail. There's another difference between the lambda calculus and the =F0-calculus. As formulated, the lambda calculus is higher order: you can pass lambda terms as arguments to lambda terms. In th= e original formulation of the =F0-calculus it is not higher order. You can pa= ss names around, but you can't pass processes around. There are higher order versions and there is a compilation scheme from higher order to name-passing. However, the higher order structure significantly changes the calculus. For example, you can get rid of replication with higher order structure. Beyond this point you have a bifurcation in the kinds of higher order calculi. In the models proposed by Sangiorgi, et al, you have two kinds of variables -- ones that carry names and ones that carry processes. To my sensibilities this is significant extra structure. In the models proposed b= y Radestock and myself, you have only 1 kind of variable, but you have reflective structure, allowing the interconversion between processes and names. This structure allows you to drop the new operator. Again, this is clearly extra structure. All in all, i think we can safely conclude that "higher order capability" i= s another difference between lambda and =F0-calculus that is not merely administrivia. Best wishes, --greg [For admin and other information see: http://www.mta.ca/~cat-dist/ ]