首页    期刊浏览 2024年11月07日 星期四
登录注册

文章基本信息

  • 标题:Bistable Biorders: A Sequential Domain Theory
  • 本地全文:下载
  • 作者:James Laird
  • 期刊名称:Logical Methods in Computer Science
  • 印刷版ISSN:1860-5974
  • 电子版ISSN:1860-5974
  • 出版年度:2007
  • 卷号:3
  • 期号:02
  • DOI:10.2168/LMCS-3(2:5)2007
  • 出版社:Technical University of Braunschweig
  • 摘要:

    We give a simple order-theoretic construction of a Cartesian closed category of sequential functions. It is based on bistable biorders, which are sets with a partial order -- the extensional order -- and a bistable coherence, which captures equivalence of program behaviour, up to permutation of top (error) and bottom (divergence). We show that monotone and bistable functions (which are required to preserve bistably bounded meets and joins) are strongly sequential, and use this fact to prove universality results for the bistable biorder semantics of the simply-typed lambda-calculus (with atomic constants), and an extension with arithmetic and recursion. We also construct a bistable model of SPCF, a higher-order functional programming language with non-local control. We use our universality result for the lambda-calculus to show that the semantics of SPCF is fully abstract. We then establish a direct correspondence between bistable functions and sequential algorithms by showing that sequential data structures give rise to bistable biorders, and that each bistable function between such biorders is computed by a sequential algorithm.

  • 关键词:Domain Theories;Functional Programming;Data Structures;Algorithms
国家哲学社会科学文献中心版权所有