[TYPES] models of untyped lambda calculus

Rosu, Grigore grosu at illinois.edu
Sun Sep 16 18:29:39 EDT 2018

Are there conventional models of untyped lambda calculus for which equational deduction with alpha+beta is *complete*?  By conventional models I mean ones where lambda and application are interpreted as functions.
The Hindley-Longo style models are complete but non-conventional.  On the other hand, graph models are conventional but incomplete.

Thank you,

More information about the Types-list mailing list