We give a category-theoretic formulation of Engeler-style models for the untyped A-calculus. In order to do so, we exhibit an equivalence between distributive laws and extensions of one monad to the Kleisli category o...
详细信息
We give a category-theoretic formulation of Engeler-style models for the untyped A-calculus. In order to do so, we exhibit an equivalence between distributive laws and extensions of one monad to the Kleisli category of another and explore the example of an arbitrary commutative monad together with the monad for commutative monoids. On Set as base category, the latter is the finite multiset monad. We exploit the self-duality of the category Rel, i.e., the Kleisli category for the powerset monad, and the category theoretic structures on it that allow us to build models of the untyped lambda-calculus, yielding a variant of the Engeler model. We replace the monad for commutative monoids by that for idempotent commutative monoids, which, on Set, is the finite powerset monad. This does not quite yield a distributive law, so requires a little more subtlety, but, subject to that subtlety, it yields exactly the original Engeler construction.
We present a new denotational model for the untyped lambda-calculus, using the techniques of game semantics. The strategies used are innocent in the sense of Hyland and Ong (Inform. and Comput., to appear) and Nickau ...
详细信息
We present a new denotational model for the untyped lambda-calculus, using the techniques of game semantics. The strategies used are innocent in the sense of Hyland and Ong (Inform. and Comput., to appear) and Nickau (Hereditarily Sequential Functionals: A Game-Theoretic Approach to Sequentiality, Shaker-Verlag, 1996. Dissertation, Universitat Gesamthochschule Siegen, Shaker-Verlag, 1996), but the traditional distinction between "question" and "answer" moves is removed. We first construct models D and D-REC as global sections of a reflexive object in the categories A and A(REC) of arenas and innocent and recursive innocent strategies, respectively. We show that these are sensible lambdaeta-algebras but are neither extensional nor universal. We then introduce a new representation of innocent strategies in an economical form. We show a strong connexion between the economical form of the denotation of a term in the game models and a variable-free form of the Nakajima tree of the term. Using this we show that the definable elements of D-REC are precisely what we call effectively almost-everywhere copycat (EAC) strategies. The category A(EAC) with these strategies as morphisms gives rise to a lambdaeta-model D-EAC which we show has the same expressive power as D-infinity, i.e. the equational theory of D-EAC is the maximal consistent sensible theory H*. We show that the model D-EAC is sensible, order-extensional and universal (i.e. every strategy is the denotation of some lambda-term). To our knowledge this is the first syntax-free model of the untyped lambda-calculus with the universality property. (C) 2002 Elsevier Science B.V. All rights reserved.
We show that the standard normalization-by-evaluation construction for the simply-typed lambda(beta eta)-calculus has a natural counterpart for the untypedlambda(beta)-calculus, with the central type-indexed logical ...
详细信息
We show that the standard normalization-by-evaluation construction for the simply-typed lambda(beta eta)-calculus has a natural counterpart for the untypedlambda(beta)-calculus, with the central type-indexed logical relation replaced by a "recursively defined" invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation. In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of soundness (the output term, if any, is in normal form and beta-equivalent to the input term);identification (beta-equivalent terms are mapped to the same result);and completeness (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like, call-by-value language. Finally, we generalize the construction to produce an infinitary variant of normal forms, namely Bohm trees. We show that the three-part characterization of correctness, as well as the proofs, extend naturally to this generalization.
作者:
Arrighi, PabloDowek, GillesUniv Grenoble
Lab LIG UMR 5217 220 Rue Chim F-38400 St Martin Dheres France Univ Lyon
Lab LIP UMR 5668 46 Allee Italie F-69007 Lyon France INRIA
23 Ave ItalieCS 81321 F-75214 Paris 13 France
We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher order computation and linear algebra. This language exte...
详细信息
We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher order computation and linear algebra. This language extends the lambda-calculus with the possibility to make arbitrary linear combinations of terms alpha.t + beta.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally, we prove the confluence of the entire calculus.
We show that the untyped lambda-calculus can be extended with Frege's interpretation of propositional notions, provided we restrict beta-conversion to positive expressions. The system of illative lambda-calculus s...
详细信息
We show that the untyped lambda-calculus can be extended with Frege's interpretation of propositional notions, provided we restrict beta-conversion to positive expressions. The system of illative lambda-calculus so obtained admits a natural Scott-style semantics. (c) 2008 WILEY-VCH Verlag GmbH & Co. KGaA. Weinheim.
We generalize Baeten and Boerboom's method of forcing to show that there is a fixed sequence (u(k))(k is an element of omega) of closed (untyped) lambda-terms satisfying the following properties: (a) For any count...
详细信息
We generalize Baeten and Boerboom's method of forcing to show that there is a fixed sequence (u(k))(k is an element of omega) of closed (untyped) lambda-terms satisfying the following properties: (a) For any countable sequence (g(k))(k is an element of omega) of Scott continuous functions (of arbitrary arity) on the power set of an arbitrary countable set, there is a graph model such that (lambda ***)(lambda ***)u(k) represents g(k) in the model. (b) For any countable sequence (t(k))(k is an element of omega) of Closed -terms there is a graph model that satisfies (lambda ***)(lambda ***)u(k) for all k. We apply these two results, which are corollaries of a unique theorem, to prove the existence of (1) a finitely axiomatized lambda-theory L such that the interval lattice constituted by the lambda-theories extending L is distributive;(2) a continuum of pairwise inconsistent graph theories (= lambda-theories that can be realized as theories of graph models);(3) a congruence distributive variety of combinatory algebras (lambda abstraction algebras, respectively). (c) 2005 Elsevier B.V. All rights reserved.
We generalize Baeten and Boerboom's method of forcing to show that there is a fixed sequence (u(k))(k is an element of omega) of closed (untyped) lambda-terms satisfying the following properties: (a) For any count...
详细信息
We generalize Baeten and Boerboom's method of forcing to show that there is a fixed sequence (u(k))(k is an element of omega) of closed (untyped) lambda-terms satisfying the following properties: (a) For any countable sequence (g(k))(k is an element of omega) of Scott continuous functions (of arbitrary arity) on the power set of an arbitrary countable set, there is a graph model such that (lambda ***)(lambda ***)u(k) represents g(k) in the model. (b) For any countable sequence (t(k))(k is an element of omega) of Closed -terms there is a graph model that satisfies (lambda ***)(lambda ***)u(k) for all k. We apply these two results, which are corollaries of a unique theorem, to prove the existence of (1) a finitely axiomatized lambda-theory L such that the interval lattice constituted by the lambda-theories extending L is distributive;(2) a continuum of pairwise inconsistent graph theories (= lambda-theories that can be realized as theories of graph models);(3) a congruence distributive variety of combinatory algebras (lambda abstraction algebras, respectively). (c) 2005 Elsevier B.V. All rights reserved.
暂无评论