• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>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的Hyperfinite Goi的启发，并开发了一种量化的方法，应该被理解为加权关系模型的动态版本。到目前为止，已经显示了交互图框架，以处理受约束系统ELL（基本线性逻辑）的指数，同时保持其定量方面。通过Girard调整旧的建设，可以清楚地定义“完整”指数，但以这些定量特征的成本为代价。我们在这里展示允许解释用来使用连续的证据（在测量理论意义上的有限者）的状态，而不是早期的相互作用图构造，这是这些状态是离散的（和有限的），提供全线性的模型具有二阶量化的逻辑。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号