科研之友
微信
新浪微博
Facebook
分享链接
摘要
The aim of this article is double. From one side we survey the knowledge we have acquired these last ten years about the lattice of all lambda-theories (equational extensions of untyped lambda-calculus) and the models of lambda calculus via universal algebra. This includes positive or negative answers to several questions raised in these years as well as several independent results, the state of the art about the long-standing open questions concerning the representability of lambda-theories as theories of models, and 26 open problems. On the other side, against the common belief, we show that lambda calculus and combinatory logic satisfy interesting algebraic properties. In fact the Stone representation theorem for Boolean algebras can be generalized to combinatory algebras and lambda-abstraction algebras. In every combinatory and lambda-abstraction algebra, there is a Boolean algebra of central elements (playing the role of idempotent elements in rings). Central elements are used to represent any combinatory and lambda-abstraction algebra as a weak Boolean product of directly indecomposable algebras (i.e. algebras that cannot be decomposed as the Cartesian product of two other non-trivial algebras). Central elements are also used to provide applications of the representation theorem to lambda calculus. We show that the indecomposable semantics (i.e. the semantics of lambda calculus given in terms of models of lambda calculus, which are directly indecomposable as combinatory algebras) includes the continuous, stable and strongly stable semantics, and the term models of all semisensible lambda-theories. In one of the main results of the article we show that the indecomposable semantics is equationally incomplete, and this incompleteness is as wide as possible.
- 出版日期2010-8
