User loginNavigation 
Reference and reasoning  or, how pure is the pure lambda calculus, part 2In the posting, Quotation and evaluation  or, how pure is the pure lambda calculus? (http://lambdatheultimate.org/node/1930), i mentioned that i saw quotation as a means of structuring namefree accounts of computations that provided a way of preserving the base term structure. i see preserving term structure as a very important property. In my experience an algebraic means of expressing computation comes to the fore because there is something in the syntax that aligns well with the semantics it expresses. Users, programmers, designers, analysts can think through the syntax to the semantics. So, preserving whatever it is that the syntax got right is part and parcel of preserving the arc of development of the notion of computation. Further, to my way of thinking each notion of computation is not just situated in a larger space of notions of computation but its form predicts, to a large degree, how the notion of computation will evolve, and therefore how our understanding of computation as captured in said notion evolves. The πcalculus captures computation as process. Petrinets capture computation as token flow. And, the λcalculus captures computation as (a kind of) function. To illustrate how preserving term structure sets up an arc of the development of our ideas about computation i want to reveal some structure that was already implicit in the lambda calculus. Again, i take a page from the process algebra community, who were, whether they knew it or not, taking a page from Abramsky's domain theory in logical form. Here are some relevant references: http://web.comlab.ox.ac.uk/oucl/work/samson.abramsky/dtlf.pdf and http://ctp.di.fct.unl.pt/~lcaires/papers/BehSpaObs.ps The latter shows the application of a general technique of deriving a logic from term structure to the πcalculus. The former shows the origins of thinking about such techniques. In Namespace Logic: A Logic for a Reflective HigherOrder Calculus. (Trustworthy Global Computing, International Symposium, TGC 2005, Edinburgh, UK, April 79, 2005, Revised Selected Papers; Spring er sent me this link http://dx.doi.org/10.1007/11580850_19; or try http://www.springerlink.com/content/9783540300076/ for the TGC publication), Matthias Radestock and i applied the same technique Caires does in his Behavioral and Spatial Observations paper but to a πcalculus with quotation, discovering a logic that allowed us to reason about names and name spaces. In what follows below i simply apply the technique to generate a program logic for the λcalculus with quotation that i presented in (http://lambdatheultimate.org/node/1930). Just as Howard follows Curry in the CurryHoward isomorphism, you can bet that a type system follows from this logic. In the sequel we let Λ(M) denote the set of terms generated by the following grammar
Likewise, we let Λ(^M^) denote the set of names generated by said grammar. Also, we use ≡ to denote the structural equivalence relation defined in (http://lambdatheultimate.org/node/1930). Now, we borrow another page from Caires and present simultaneously the syntax and semantics of our logic.
Discussion... first, i leave it as an exercise to the reader to add a greatest fix point formulae and its semantics to this presentation. You can crib Caires paper to get a nice clean extension. Next i submit, without proof, that pretty much all the freshness machinery coming out of Pitts and Gabbay can be captured within this framework. Now, here's one of the practical applications that has been driving a lot of this work. Suppose that you had a database of programs. (E.g., oh, say source forge, or google code base.) Now, suppose you wanted to find a program not on the basis of what the code is called, or what the variable names were, but on the basis of what the code does. This logic gives the basis for a query engine in which the structure and dynamics of programs can be queried. In a subsequent posting i will write down some interesting formulae. Let me close this posting by saying that all i am doing is applying a sequence of functors, the quotation functor, and then the logic generating functor. These functors  being functors  are preserving a certain structure, including the term structure. The sequence unveils the 'dynamics', the unfolding of the notion of computation, implicit in λcalculus. Much of this can be seen as a working out of Christopher Alexander's ideas about structure preserving processes, as he describes in the Nature of Order. By Lucius Gregory Meredith at 20061227 19:39  LtU Forum  previous forum topic  next forum topic  other blogs  3506 reads

Browse archivesActive forum topics 
Recent comments
6 days 17 hours ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 1 day ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago
1 week 2 days ago