[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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, Grigore
