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.

About Nominal Logic(s)

Hello Lucius,

I am very interested in the link you done with Nominal Logic(s).
I am studying the works of Tiu-Miller that have proof-theoretical origins but seems very close to the works of Gabbay-Pitts (semantic origins) at the end. They use Nabla where G-P uses "New".

So, please, in your next posts can you describe (without proofs) an "encoding" of New (~Nabla) within your framework?

Is there a paper(s) describing your work(s) with this version of lambda calculus?

Thanks,

Matteo

By Matteo at Fri, 2006-12-29 09:33 | login or register to post comments

Would you like the π or the λ version?

Matteo,

Many thanks for your interest. Let me know which version you want. The main thing is that you have to host the implementation of the language-level binder operation in the language itself; thus, it differs from λ to π. The logical operation can be lifted in the obvious manner.

i will mention that i did find a Galois-extension style approach that's pretty darn cool and is language independent and is independent of centralized/distributed nameserver issues that plague the concurrent setting. It's primary drawback is that it introduces non-well-founded quoting.

Here are the key intuitions. In the term grammar i gave above note that the following name cannot be produced.

^λ ^L^.x^

So, we could imagine adjoining this name to the grammar. For purposes of exposition, let's call this name λ₁. We modify the grammar by changing the production for names to

x	::=		^M^
			λ₁

Call this new language Λ(M)[λ₁]. Next, note that the following name, call it λ₂, cannot be produced by Λ(M)[λ₁].

^λ λ₁.x^

But, we can play our extension trick again, producing a new grammar, Λ(M)[λ₁][λ₂].

Notice that there are natural embeddings of our term languages into the extended term languages. Thus, there is a natural way to interpret the natural isomorphisms up and swap. This should be sufficient to get you going. If not, feel free to ping me again.

(i feel compelled to point out that Dusko Pavlovic worked out a more abstract, but similar set of intuitions in a treatment of action calculi like widgets. But, i'm going to have to dig around for the reference (found it: Categorical logic of names and abstraction in action calculi; http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=44693). i confess i didn't try very hard, but i couldn't get the hang of his calculations. Mine, as you can see, are dirt simple.)

Finally, let me point out that there is a limit to our adjoining procedure.

x	::=	^M^	// a name is a quoted term, or
		rec α.^M^	// recursively defined quoted term
		α

This limit lets loose all kinds of beasties; so, i've not explored it vigorously.

By Lucius Gregory Meredith at Fri, 2006-12-29 16:34 | login or register to post comments

Lambda the Ultimate

User login

Navigation