BROADCASTS.com

b'

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').\\xa0 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.\\xa0 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).