论H*模型的特征刻画：语义视角
计算机科学中的逻辑
2019-03-14 v2
摘要
针对无类型lambda演算的一大类模型，我们给出了那些对头规范化（head-normalization）完全抽象的模型的特征刻画，即其等式理论为H*（头规范化的观测）。一个外延K模型是完全抽象的，当且仅当它是超免疫的（hyperimmune），亦即，D中元素的非良基链无法被任何递归函数所捕获。本文与其姊妹篇共同构成[Bre14]的长版本。它是一篇独立论文，给出了该结果的纯语义证明，而其姊妹篇给出了同一结果的独立且纯语法的证明。
引用
@article{arxiv.1603.07259,
title = {On the characterization of models of H*: The semantical aspect},
author = {Flavien Breuvart},
journal= {arXiv preprint arXiv:1603.07259},
year = {2019}
}