通过博弈语义研究二阶类型同构
计算机科学中的逻辑
2007-05-30 v1
摘要
二阶类型同构的刻画是一个纯粹语法性的问题,我们提议在博弈语义的启发下对其进行研究。我们在二阶 λμ-演算(可视为系统 F 向经典逻辑的扩展)的框架下考察此问题,并为之定义了一个范畴论框架:控制超 doctrines。我们对 λμ-演算的博弈模型基于多态 arena(与 Hughes 的超森林密切相关),其在博弈过程中会演化(沿袭 Murawski-Ong 的思想)。我们证明类型同构与 arena 上由类型诱导的"相等"关系一致,并由此推导出类型同构的等式刻画。借助同一模型,我们还重新得到了 Roberto Di Cosmo 对系统 F 类型同构的刻画。该方法为二阶类型同构问题提供了几何层面的理解,并可方便地推广到包含其他编程特征的一些多态演算。
引用
@article{arxiv.0705.4226,
title = {Second-Order Type Isomorphisms Through Game Semantics},
author = {Joachim De Lataillade},
journal= {arXiv preprint arXiv:0705.4226},
year = {2007}
}
评论
accepted by Annals of Pure and Applied Logic, Special Issue on Game Semantics