检索结果-内蒙古大学图书馆

A Category Theoretic Formulation for Engeler-style Models of the untyped lambda-calculus

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第1期161卷 43-57页

作者： Hyland, Martin x Nagayama, Misao Power, John Rosolini, Giuseppe Univ Cambridge Dept Pure Math & Math Stat Wilberforce Rd Cambridge CB30WB England Japan Sci & Technology Corp Res Ctr Verificat & Semant CVS Natl Inst Adv Ind Sci & Technol AIST CREST Amagasaki Hyogo 6610974 Japan Univ Edinburgh Lab Foundat Comp Sci Edinburgh EH9 3JZ Midlothian Scotland Univ Genoa DISI I-16146 Genoa Italy

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.

关键词： Engeler model untyped lambda-calculus cartesian closed category distributive law commutative monoid finite multiset finite powerset Kleisli construction

来源：评论

学校读者我要写书评

暂无评论

Innocent game models of untyped λ-calculus

引用

THEORETICAL COMPUTER SCIENCE 2002年第1-2期272卷 247-292页

作者： Ker, AD Nickau, H Ong, CHL Univ Oxford Comp Lab Oxford OX1 3QD England

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.

关键词： game semantics innocent strategies untyped lambda-calculus

来源：评论

学校读者我要写书评

暂无评论

Denotational aspects of untyped normalization by evaluation

Denotational aspects of untyped normalization by evaluation

引用

7th International Conference on Foundations of Software Science and Computation Structures

作者： Filinski, A Rohde, HK Univ Copenhagen Dept Comp Sci DIKU DK-2100 Copenhagen Denmark Univ Aarhus Dept Comp Sci BRICS IT Parken DK-8200 Aarhus Denmark

We show that the standard normalization-by-evaluation construction for the simply-typed lambda(beta eta)-calculus has a natural counterpart for the untyped lambda(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.

关键词： normalization by evaluation untyped lambda-calculus denotational semantics functional programming Bohm trees computational adequacy

来源：评论

学校读者我要写书评

暂无评论

LINEAL: A LINEAR-ALGEBRAIC λ-calculus

引用

LOGICAL METHODS IN COMPUTER SCIENCE 2017年第1期13卷

作者： Arrighi, Pablo Dowek, Gilles Univ 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 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.

关键词： rewrite systems untyped lambda-calculus quantum programming languageses

来源：评论

学校读者我要写书评

暂无评论

Positive Frege and its Scott-style semantics

引用

MATHEMATICAL LOGIC QUARTERLY 2008年第4期54卷 410-434页

作者： Libert, Thierry Univ Libre Bruxelles Dept Math B-1050 Brussels Belgium

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... 详细信息

关键词： Frege's system untyped lambda-calculus positive set theory

来源：评论

学校读者我要写书评

暂无评论

Easiness in graph models

引用

THEORETICAL COMPUTER SCIENCE 2006年第1期354卷 4-23页

作者： Berline, C Salibra, A CNRS F-72251 Paris 05 France Univ Paris 07 F-72251 Paris 05 France Univ Ca Foscari Venezia Dipartimento Informat I-30172 Venice Italy

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.

关键词： untyped lambda-calculus graph models easy terms Scott's continuous semantics lattice of lambda-theories webbed models combinatory algebras lambda abstraction algebras

来源：评论

学校读者我要写书评

暂无评论

Easiness in graph models

Easiness in graph models

引用

3rd International Workshop on Algebraic Methods in Language Processing

作者： Berline, C Salibra, A CNRS F-72251 Paris 05 France Univ Paris 07 F-72251 Paris 05 France Univ Ca Foscari Venezia Dipartimento Informat I-30172 Venice Italy

关键词： untyped lambda-calculus graph models easy terms Scott's continuous semantics lattice of lambda-theories webbed models combinatory algebras lambda abstraction algebras

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：