• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>情報処理学会論文誌 >ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States
【24h】

ML, Visibly Pushdown Class Memory Automata, and Extended Branching Vector Addition Systems with States

机译：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.
机译：我们证明，编程语言ML的最后一个片段的观测等价问题递归等效于带状态的扩展分支向量加法系统（EBVASS）的可达性问题。这个结果有两个自然的和独立的部分。我们首先证明，观测等价问题等同于配备了可见下推堆栈的新型类存储自动机的空性问题，称为可视下推类存储自动机（VPCMA）。我们的证明使用了语言的完全抽象的游戏语义。然后，我们证明VPCMA空度问题等同于EBVASS的可达性问题。本文的结果完善了我们的程序，以针对封闭项的观测等价问题给出ML类型的自动机分类。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号