Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (similar to a definition in John C. Mitchell's book "Foundations for Programming Languages').  In short, lambda abstractions get interpreted in combinatory algebras by compiling away the lambda abstractions in favor of S and K combinators, which are then interpreted by the combinatory algebra.  I complain about the fact that the definition of a lambda applicative structure is required to come with an interpretation function for terms (hence tying the semantics to the syntax).

Ver todos los episodios