Skip navigation

Category Archives: Lambda Calculus

I remember, from maybe grad school, being puzzled about “semantics”.  What does this word mean?  Having gained a lot more knowledge of this topic since then, I thought I’d share a few thoughts on it, especially in the context of type theory.

“Semantics” means meaning.  In this sense, many different approaches to the study of programming languages are described as giving some form of semantics to a language.  An interpreter gives you a semantics for a language.  It shows you what these funny sequences of keywords or symbols (or more modernly, these peculiar abstract syntax trees) mean by showing how the programs execute.  If one writes an interpreter as a set of inference rules, then this is usually called operational semantics.  Hoare Logic, which is a set of inference rules for verifying that programs started in states satisfying a given precondition will (if they terminate) end in a state satisfying a given postcondition, has traditionally been dubbed axiomatic semantics.  This term “axiomatic” is maybe not too informative, but the idea that you can describe the meaning of an imperative program by explaining how it changes the state indeed gives it a reasonable claim to be a semantics.  What do programs in the language mean?  A semantics tells you.

There was a lot of interest in earlier days on giving denotational semantics to programs.  The idea is to give the meaning of a program by stating what mathematical function the program denotes.  After all, programs are intended (are they not?) to represent some class of functions as understood in mathematics.  A hallmark of denotational semantics is that it is compositional: the meaning of a bigger expression is defined in terms of the meanings of its strict subexpressions.  Notice that this is not true of operational semantics generally: we define the meaning of (\lambda x.\, t)\ t' in terms of [t'/x]t, which is not a strict subexpression of t (indeed it can be a bigger term than t). There was a lot of excitement, it seems, in finding denotational models of languages like lambda calculus.  More recently, it seems more common, at least in Computer Science, to take lambda calculus for granted and not be concerned with mathematical denotations of lambda terms.

Logic is, as far as I know, the earliest field concerned with giving mathematical semantics for formal languages.  There, denotational semantics of formulas is the basis of model theory.  Proof theory can also be viewed as giving a semantics of formulas, and indeed in nice situations these two semantics agree — though even for theories like first-order arithmetic, results like Goedel’s incompleteness theorem imply that no such agreement is possible: the proof-theoretic semantics (showing what formulas mean by showing how to prove them or use them in other proofs) must be weaker, in the sense of proving fewer theorems, than the denotational semantics.  But maybe this is a digression…

In type theory, there is a great tradition of giving denotational semantics for types.  In full generality, if we have a term t of type T (in some typing context G!), we would like to explain what this relation (G \vdash t : T) means.  Historically, it was discovered that one could use a denotational semantics for types as a proof method to show deep properties of the language, like normalization or logical consistency.  I first learned about this in Girard’s Proofs and Types, and still recommend this as a good introduction.  The historical root of this is Kleene’s realizability semantics for first-order intuitionistic arithmetic.  But one does not need to be driven by the desire to prove such metatheorems, in order to want to have a denotational semantics for types.  Here are my amazing new types!  Wouldn’t you like to know what they mean?  I can show you some typing rules, and depending on how I set them up — for example, if you give introduction and elimination rules for the types that are related in certain ways — these could to a greater or lesser extent show you what the types mean.  But a compositional semantics that says, “my funny type construct X A B means …” can be more direct, and provide guidance for crafting typing rules.  One can prove that a set of typing rules is sound with respect to the semantics, for example.

The form of such semantics I have found most useful is a realizability semantics, that tells you what a type means by specifying the set of all terms whose operational behavior is allowed by the type.  For example, in some language, the meaning of a type like “Int -> Int” could be defined to be the set of all programs which, given an Int input, either diverge or produce an Int output.  Or maybe in some other language, it is the set of all terms which, given an Int input, are guaranteed to terminate producing an Int output.  Notice that these example semantics do not say anything about the internal form of the program.  It could fail to be well-typed according to some set of typing rules.  It could do very crazy and upsetting things if not given an Int input.  The only thing the type specifies is the behavior of the term when given an Int input.  So the type describes behavior of terms, through the simple device of giving a set of terms as the meaning of a type (namely, the set of all terms whose behavior is allowed by the type).

For Cedille, I have defined such a semantics, and used it to prove logical consistency of the system.

Advertisements

This past Tuesday (June 19) I gave the second lecture in the series I am working on, about optimal beta-reduction.  The screencast can be found here.  This lecture covers the basic nondeterministic graph reduction rules for lazy duplication.  The notes you will see my writing are here in ora and jpeg formats.  The lambdascope implementation I try using (and many thanks to Jan Rochel for this!) can be found here on hackage.  The lambdascope paper can be found here.

It is a warm start to summer here in Iowa, and among other interesting things to think about, I have been studying the subject of optimal beta-reduction, which has been developed from Jean-Jacques Levy’s dissertation in the 1970s to John Lamping’s 1990 POPL paper, and beyond.  I am using an amazing book by Andrea Asperti and Stefano Guerrini: The Optimal Implementation of Functional Programming Languages.

To help myself learn this, I am giving (and have decided to record) some lectures on the topic.  I am definitely not an expert, only an aspirant!  If you happen to watch these and find errors or confusions, please correct me.  The screencast for the first lecture, covering some main points of Chapter 2 of Asperti and Guerrini, is here.  The notes you will see me writing in the screencast are here, in jpg and ora formats.

I am interested in this because my friend Victor Maia of Ethereum Foundation is considering using a variant of Lamping’s abstract algorithm to run smart contracts in Ethereum, to be written in pure lambda calculus and verified with Cedille (the tool we are working on here now the past few years).

When you hear “Craig’s Theorem”, you probably think of the Craig Interpolation Theorem, and rightly so.  This is the most famous theorem (I suppose) of philosopher and logician William Craig.  So I was surprised to find out there is another “Craig’s Theorem” that is even cooler for those of us interested in lambda calculus.  It is well known that every lambda term can be simulated using a combinator term written using combinators S and K.  Have you ever wondered if there is a way to simulate all lambda terms using just a single proper combinator Q (proper here means that the combinator is defined by a reduction rule showing how to reduce Q\ x_1\ \ldots\ x_k to some term built from applications of the variables x_1, \ldots, x_k)?  Craig’s (other) Theorem says no.  There is a very short (2 pages) proof given here (sorry, this is behind a paywall, I think).  I can give a simple variation of this proof here.

Suppose there were such a combinator Q.  Since it is, by assumption, combinatorily complete, there must be some way to write the identity combinator I using just Q.  Consider the reduction sequence I\ x\ \to^* M\ \to\ x, where M\ \to \ x is the last step in this reduction sequence (which must be of length at least one since I\ x is not the same as x).  Since M reduces, it must be of the form Q\ c_1\ \ldots\ c_n for some combinators c_1,\ldots,c_n.  But this tells us that Q must be projecting one of the inputs c_1,\ldots,c_n to the final result (and one of those c_i must be x).  So Q is a projection combinator.   This part is from the linked paper by Bellot.  Here is now an alternative conclusion.  If a sequence of reductions consists solely of projections of inputs, then that sequence must be terminating, because at each step, the size of the term is decreased by doing a projection.  But the lambda calculus includes nonterminating terms, so a projection function cannot be a sufficient basis for the lambda calculus.  Hence there is no one-combinator basis for the lambda calculus (and we need at least two, such as S and K).

Fun stuff!