archives

Reference and reasoning -- or, how pure is the pure lambda calculus, part 2

In the posting, Quotation and evaluation -- or, how pure is the pure lambda calculus? (http://lambda-the-ultimate.org/node/1930), i mentioned that i saw quotation as a means of structuring name-free 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. Petri-nets 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 Higher-Order Calculus. (Trustworthy Global Computing, International Symposium, TGC 2005, Edinburgh, UK, April 7-9, 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/978-3-540-30007-6/ 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://lambda-the-ultimate.org/node/1930). Just as Howard follows Curry in the Curry-Howard 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

M,N ::= x // terms are names
P // or programs
P ::= L // programs are the ur-program, L
λx.M // or abstractions
MN // or applications
*x // or unquoted or 'dropped' names
x ::= ^P^ // names are quoted programs

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://lambda-the-ultimate.org/node/1930). Now, we borrow another page from Caires and present simultaneously the syntax and semantics of our logic.

⌈ T ⌉ = Λ(M) // verity denotes the entire set of terms, or if you like all terms satisfy T
⌈ ~φ ⌉ = Λ(M) \ ⌈ φ ⌉ // negation is complement in the universe of terms
⌈ φ ∧ ψ ⌉ = ⌈ φ ⌉ ∩ ⌈ ψ ⌉ // conjunction is intersection
⌈ L ⌉ = { t ∈ Λ(M) | t ≡ L } // we have another constant, this one picks out terms structurally equivalent to the ur-program, L
⌈ λa.φ ⌉ = { t ∈ Λ(M) | t ≡ λx.u, x ∈ ⌈ a ⌉, u ∈ ⌈ φ ⌉ } // we can pick out terms that are abstractions
⌈ φψ ⌉ = { t ∈ Λ(M) | t ≡ uv, u ∈ ⌈ φ ⌉, v ∈ ⌈ ψ ⌉ } // we can pick out terms that are applications
⌈ 〈ψ〉φ ⌉ = { t ∈ Λ(M) | ∃u ∈ ⌈ ψ ⌉. tu → v, v ∈ ⌈ φ ⌉ } // this is our only behavioral formulae, it uses application as observation, and is related to residuation
⌈ *a ⌉ = { t ∈ Λ(M) | t ≡ *x, x ∈ ⌈ a ⌉ } // we can pick out dropped terms
⌈ ∀n∈^ψ^.φ ⌉ = ∩v∈ ⌈ ^ψ^ ⌉ ⌈ φ[v/n] ⌉ // we quantify over the structure of variables
⌈ ^φ^ ⌉ = { x ∈ Λ(^M^) | x ≡ ^N^, N ∈ ⌈ φ ⌉ } // we can pick out sets of variables, alternatively, we can identify variable shapes

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 2006-12-27 19:39 | LtU Forum | 2 comments | other blogs | 5234 reads