Curry 风格类型同构与博弈语义
计算机科学中的逻辑
2007-05-30 v1
摘要
Curry 风格系统 F,即项中不显式标注类型的系统 F,可被视为从编程语言视角对多态性的一种核心表述。本文通过使用一种博弈模型来刻画该语言的类型同构,该模型的直觉既来自语法,也来自博弈语义领域。该模型由以下部分组成:用于解释项的无类型部分、用于解释类型的博弈概念,以及用于表达无类型策略在博弈上进行博弈的有类型部分。通过分析模型中的同构关系,我们证明了对应于 Curry 风格系统 F 类型同构的等式系统,是 Church 风格同构等式系统扩展了一条新的非平凡等式后的结果:若 X 仅在 A 中正性出现,则 forall X.A = A[forall Y.Y/X]。
引用
@article{arxiv.0705.4228,
title = {Curry-style type Isomorphisms and Game Semantics},
author = {Joachim De Lataillade},
journal= {arXiv preprint arXiv:0705.4228},
year = {2007}
}
评论
Accept\'e \`a Mathematical Structures for Computer Science, Special Issue on Type Isomorphisms