The sensible graph theories of lambda calculus Bucciarelli, A.; Salibra, A.
Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 2004,
2004
Conference Proceeding
Odprti dostop
Sensible /spl lambda/-theories are equational extensions of the untyped lambda calculus that equate all the unsolvable /spl lambda/-terms and are closed under derivation. A longstanding open problem ...in lambda calculus is whether there exists a non-syntactic model whose equational theory is the least sensible /spl lambda/-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of models, there exist a minimal and maximal sensible /spl lambda/-theory represented by it. In This work we give a positive answer to this question for the semantics of lambda calculus given in terms of graph models. We conjecture that the least sensible graph theory, where "graph theory" means "/spl lambda/-theory of a graph model", is equal to H, while in the main result of the paper we characterize the greatest sensible graph theory as the lambda;-theory B generated by equating /spl lambda/-terms with the same Bohm tree. This result is a consequence of the fact that all the equations between solvable /spl lambda/-terms, which have different Bohm trees, fail in every sensible graph model. Further results of the paper are: (i) the existence of a continuum of different sensible graph theories strictly included in B (this result positively answers question 2 in 7, Section 6.3); (ii) the non-existence of a graph model whose equational theory is exactly the minimal lambda theory /spl lambda//spl beta/ (this result negatively answers Question 1 in 7, Section 6.2 for the restricted class of graph models).
Lambda abstraction algebras (LAAs) are designed to algebraize the untyped lambda calculus in the same way cylindric and polyadic algebras algebraize the first-order predicate logic. Like combinatory ...algebras they can be defined by true identities and thus form a variety in the sense of universal algebra, but they differ from combinatory algebras in several important respects. The most natural LAAs are obtained by coordinatizing environment models of the lambda calculus. This gives rise to two classes of LAAs of functions of finite arity:
functional LAAs (FLA) and
point-relativized functional LAAs (RFA). It is shown that RFA is a variety and is the smallest variety including FLA.
Dimension-complemented LAAs constitute the widest class of LAAs that can be represented as an algebra of functions and are known to have a natural intrinsic characterization. We prove that every dimension-complemented LAA is isomorphic to RFA. This is the crucial step in showing that RFA is a variety.
After Scott, mathematical models of the type-free lambda calculus are constructed by order theoretic methods and classified into semantics according to the nature of their representable functions. ...Selinger 48 asked if there is a lambda theory that is not induced by any non-trivially partially ordered model (order-incompleteness problem). In terms of Alexandroff topology (the strongest topology whose specialization order is the order of the considered model) the problem of order-incompleteness can be also characterized as follows: a lambda theory T is order-incomplete if, and only if, every partially ordered model of T is partitioned by the Alexandroff topology in an infinite number of connected components (= minimal upper and lower sets), each one containing exactly one element of the model. Towards an answer to the order-incompleteness problem, we give a topological proof of the following result: there exists a lambda theory whose partially ordered models are partitioned by the Alexandroff topology in an infinite number of connected components, each one containing at most one λ-term denotation. This result implies the incompleteness of every semantics of lambda calculus given in terms of partially ordered models whose Alexandroff topology has a finite number of connected components (e.g.the Alexandroff topology of the models of the continuous, stable and strongly stable semantics is connected).
A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the least lambda-theory lambda-beta or the least ...sensible lambda-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we give a general tool to answer positively to this question and we apply it to a wide class of webbed models: the i-models. The method then applies also to graph models, Krivine models, coherent models and filter models. In particular, we build an i-model whose theory is the set of equations satisfied in all i-models.
We introduce a functional calculus with simple syntax and operational semantics in which the calculi introduced so far in the Curry-Howard correspondence for Classical Logic can be faithfully ...encoded. Our calculus enjoys confluence without any restriction. Its type system enforces strong normalization of expressions and it is a sound and complete system for full implicational Classical Logic. We give a very simple denotational semantics which allows easy calculations of the interpretation of expressions.
The Abstract Variable-Binding Calculus Pigozzi, Don; Salibra, Antonino; Salibra, Antonio
Studia logica,
07/1995, Letnik:
55, Številka:
1
Journal Article
Recenzirano
The abstract variable binding calculus (VB-calculus) provides a formal framework encompassing such diverse variable-binding phenomena as lambda abstraction, Riemann integration, existential and ...universal quantification (in both classical and nonclassical logic), and various notions of generalized quantification that have been studied in abstract model theory. All axioms of the VB-calculus are in the form of equations, but like the lambda calculus it is not a true equational theory since substitution of terms for variables is restricted. A similar problem with the standard formalism of the first-order predicate logic led to the development of the theory of cylindric and polyadic Boolean algebras. We take the same course here and introduce the variety of polyadic VB-algebras as a pure equational form of the VB-calculus. In one of the main results of the paper we show that every locally finite polyadic VB-algebra of infinite dimension is isomorphic to a functional polyadic VB-algebra that is obtained from a model of the VB-calculus by a natural coordinatization process. This theorem is a generalization of the functional representation theorem for polyadic Boolean algebras given by P. Halmos. As an application of this theorem we present a strong completeness theorem for the VB-calculus. More precisely, we prove that, for every VB-theory T that is obtained by adjoining new equations to the axioms of the VB-calculus, there exists a model D such that$\vdash _{\text{T}}s=t$iff$\vDash _{\text{D}}s=t$. This result specializes to a completeness theorem for a number of familiar systems that can be formalized as VB-calculi. For example, the lambda calculus, the classical first-order predicate calculus, the theory of the generalized quantifier exists uncountably many and a fragment of Riemann integration.
PDF
