ORDERED MODELS OF THE LAMBDA CALCULS
Answering a question by Honsell and Plotkin, we show that there are two equations between lambda-terms, the so-called subtractive equations, consistent with lambda-calculus but not simultaneously satisfied in any partially ordered model with bottom element. We also relate the subtractive equations to the open problem of the order-incompleteness of lambda-calculus, by studying the connection between the notion of absolute unorderability in a specific point and a weaker notion of subtractivity (namely n-subtractivity) for partially ordered algebras. Finally we study the relation between n-subtractivity and relativized separation conditions in topological algebras, obtaining an incompleteness theorem for a general topological semantics of lambda-calculus.
partially ordered models order-incompleteness lambda calculus topological models equational consistency