首页> 外文期刊>Theoretical computer science >Decidability and syntactic control of interference
【24h】

Decidability and syntactic control of interference

机译:干扰的可判定性和语法控制

获取原文
获取原文并翻译 | 示例
       

摘要

We investigate the decidability of observational equivalence and approximation in Reynolds' "Syntactic Control of Interference" (SCI), a prototypical functional-imperative language in which covert interference between functions and their arguments is prevented by the use of an affine typing discipline. By associating denotations of terms in a fully abstract "relational" model of finitary basic SCI (due to Reddy) with multitape finite state automata, we show that observational approximation is not decidable (even at first order), but that observational equivalence is decidable for all terms. We then consider the same problems for basic SCI extended with non-local control in the form of backwards jumps. We show that both observational approximation and observational equivalence are decidable in this "observably sequential" version of the language by describing a fully abstract games model in which strategies are regular languages. (C) 2007 Elsevier B.V. All rights reserved.
机译:我们研究了雷诺兹的“干扰的句法控制”(SCI)中观察等效性和近似性的可判定性,这是一种原型功能性命令性语言,其中通过使用仿射类型规制来防止功能及其参数之间的隐性干扰。通过将最终基本SCI(归因于Reddy)的完全抽象“关系”模型中的术语表示与多带有限状态自动机相关联,我们表明观察近似不是可决定的(即使是一阶的),但观察等价对于所有条款。然后,我们考虑使用非本地控制以向后跳转的形式扩展基本SCI的相同问题。我们通过描述策略为常规语言的完全抽象游戏模型,表明在这种“可观察的顺序”版本的语言中,观察近似和观察等效是可决定的。 (C)2007 Elsevier B.V.保留所有权利。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号