What’s solvability? For some terms of the pure lambda calculus reduction does not terminate. But these non-terminating terms are not the same garbage. If we equate them we obtain an inconsistent proof-theory. Indeed, some non-terminating terms are nevertheless useful if used as functions. More precisely, when applying these non-terminating terms to suitable operands we get back terminating results. (You’ve got to find this at least somewhat interesting.)

The set of solvables is made of terminating terms (which include normal forms) and those useful non-terminating terms. The rest are unsolvables which are the same garbage: equating them gives rise to a consistent proof theory.

Solvability has been studied in the pure “lambda-value” calculus that (broadly speaking) tries to model call-by-value evaluation. The problem is that the resulting proof-theory is not ‘quite’ consistent and some normal forms are unsolvable.

We did some exegetical work and found out the problem was with the use of a definition unsuited for pure lambda-value. We fixed this and got not only a consistent proof-theory but some extra results about lambda-value and full-reduction with open terms. In the process we learned a few sad lessons about social aspects of research.

Content of the Talk:

• Slide 1: Title
• Slides 2-8: Introduction to pure lambda calculus: syntax, terms, self-application (oops), reduction & conversion, normal forms, consistency.
• Slides 9-11: Solvability in the pure lambda calculus.
• Slides 12-13: The pure lambda-value calculus and what’s meant for.
• Slides 14-15: Problems with v-solvability in pure lambda-value.
• Slides 16-18: Alternative definition (back to basics), contribs, and intuition to take home.
• Slide 19: (Non)Conclusions.

Complemented with hopefully explanatory verbosity.