一句话：证明 ML 有穷片段的可观察等价问题递归等价于 EBVASS 可达性，并用 VPCMA 给出自动机刻画。
本文研究 ML（元语言）一个 finitary fragment 的观察等价（observational equivalence）问题的可判定性与复杂度定位。作者利用该语言的 fully abstract game semantics，先把闭项的观察等价归约为一种新自动机——带 visibly pushdown stack 的 class memory automata（VPCMA）的空性问题；随后证明 VPCMA 空性问题与 extended branching vector addition systems with states（EBVASS）可达性问题递归等价，因此 ML 片段的观察等价问题也与 EBVASS 可达性问题递归等价。该结果完成了此前按 ML 类型对闭项观察等价问题进行自动机分类的计划，并为相关问题建立了自动机与向量加法系统之间的精确对应。
We prove that the observational equivalence problem for a finitary fragment of the programming langauge ML is recursively equivalent to the reachability problem for extended branching vector addition systems with states (EBVASS). This result has two natural and independent parts. We first prove that the observational equivalence problem is equivalent to the emptiness problem for a new class of class memory automata equipped with a visibly pushdown stack, called Visibly Pushdown Class Memory Automata (VPCMA). Our proof uses the fully abstract game semantics of the language. We then prove that the VPCMA emptiness problem is equivalent to the reachability problem for EBVASS. The results of this article complete our programme to give an automata classification of the ML types with respect to the observational equivalence problem for closed terms.
DOI 原文 ·
@article{paperbot712,
title = {ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States},
author = {Conrad Cotton-Barratt and Andrzej S. Murawski and C.-H. Luke Ong},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {41},
number = {2},
year = {2019},
doi = {10.1145/3310338}
}