Lambda Definability with Sums via Grothendieck Logical Relations
Lambda Definability with Sums via Grothendieck Logical Relations
复制标题
通过 Grothendieck 逻辑关系求和的 Lambda 可定义性
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
A. Simpson
中科院分区：
文献类型：
--
作者：
M. Fiore;A. Simpson
本文引入Grothendieck逻辑关系的概念，并利用有限积和有限和的简单型lambda演算来证明稳定双笛卡尔闭范畴中态射的可定义性.我们的技术是基于从拓扑理论的概念，但我们的论述是基本的。
We introduce a notion of Grothendieck logical relation and use it to characterise the definability of morphisms in stable bicartesian closed categories by terms of the simply-typed lambda calculus with finite products and finite sums. Our techniques are based on concepts from topos theory, however our exposition is elementary.