一句话：研究 lambda 演算的关系图模型，证明其诱导理论有最小元，并刻画对 H+ 与 H* 完全抽象性的模型条件。
本文研究 lambda 演算关系模型的一类自然子类——关系图模型。作者首先证明，由关系图模型诱导的 lambda 理论中存在一个最小理论，并构造出一个自然且易于定义的关系图模型来实现它。随后转向完全抽象性，即模型能否精确刻画 lambda 项之间的观测等价。论文聚焦两种主要观测等价：以 beta-正规形为观测的 H+，以及以头正规形为观测的 H*。作者引入 lambda-König 模型这一概念，证明关系图模型对 H+ 完全抽象当且仅当它是扩展的且为 lambda-König 模型；并证明其对偶概念 hyperimmune 模型与扩展性一起，恰好刻画对 H* 的完全抽象。该结果为关系图模型的完全抽象性提供了精确的语义特征。
We study the relational graph models that constitute a natural subclass of relational models of lambda-calculus. We prove that among the lambda-theories induced by such models there exists a minimal one, and that the corresponding relational graph model is very natural and easy to construct. We then study relational graph models that are fully abstract, in the sense that they capture some observational equivalence between lambda-terms. We focus on the two main observational equivalences in the lambda-calculus, the theory H+ generated by taking as observables the beta-normal forms, and H* generated by considering as observables the head normal forms. On the one hand we introduce a notion of lambda-K\"onig model and prove that a relational graph model is fully abstract for H+ if and only if it is extensional and lambda-K\"onig. On the other hand we show that the dual notion of hyperimmune model, together with extensionality, captures the full abstraction for H*.
@article{paperbot393,
title = {Relational Graph Models at Work},
author = {Flavien Breuvart and Giulio Manzonetto and Domenico Ruoppolo},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 3},
year = {2018},
doi = {10.23638/lmcs-14(3:2)2018}
}