• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Interaction Graphs: Full Linear Logic
【24h】

Interaction Graphs: Full Linear Logic

机译：交互图：全线性逻辑

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Interaction graphs were introduced as a general, uniform, construction of dynamic models of linear logic, encompassing all Geometry of Interaction (GoI) constructions introduced so far. This series of work was inspired from Girard's hyperfinite GoI, and develops a quantitative approach that should be understood as a dynamic version of weighted relational models. Until now, the interaction graphs framework has been shown to deal with exponentials for the constrained system ELL (Elementary Linear Logic) while keeping its quantitative aspect. Adapting older constructions by Girard, one can clearly define "full" exponentials, but at the cost of these quantitative features. We show here that allowing interpretations of proofs to use continuous (yet finite in a measure-theoretic sense) sets of states, as opposed to earlier Interaction Graphs constructions were these sets of states were discrete (and finite), provides a model for full linear logic with second order quantification.
机译：交互图是作为线性逻辑动态模型的一般，统一，构造而引入的，涵盖了到目前为止介绍的所有交互几何（GoI）构造。该系列工作的灵感来自吉拉德（Girard）的超限GoI，并开发了一种定量方法，应将其理解为加权关系模型的动态版本。到目前为止，交互图框架已显示为处理约束系统ELL（基本线性逻辑）的指数，同时保持其定量方面。改用吉拉德（Girard）的旧结构，可以清楚地定义“完整”指数，但要以牺牲这些定量特征为代价。我们在这里表明，允许证明的解释使用连续的（在量度论意义上是有限的）状态集，与早期的交互图构造相反，这些状态集是离散的（并且是有限的），提供了全线性模型具有二阶量化的逻辑。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号