Ensuring Streams Flow
Ensuring Streams Flow
复制标题
确保溪流畅通
DOI：
10.1007/bfb0000493
复制
发表时间：
1997
影响因子：
3.2
通讯作者：
D. Turner
中科院分区：
文献类型：
--
作者：
Alastair J. Telford;D. Turner
我们的目标是开发基本强大的功能编程（ESFP）系统。为了有用，ESFP应包括可以在计算上无限频繁地计算的流中的结构。我们描述了句法分析，以确保无限进行的结构（我们将定为码头）是有效的。该分析是对守卫的检查的扩展，该检查已与Martin-Lof类型理论和结构计算中的定义一起使用。我们的分析被称为抽象解释的一种形式，该形式允许将更广泛的句法类别的定义识别为比以前的工作相比。因此，程序员在强烈正常化的功能语言中使用无限流的限制将更少。
It is our aim to develop an elementary strong functional programming (ESFP) system. To be useful, ESFP should include structures such as streams which can be computationally unwound infinitely often. We describe a syntactic analysis to ensure that infinitely proceeding structures, which we shall term codata, are productive. This analysis is an extension of the check for guardedness that has been used with definitions over coinductive types in Martin-Lof's type theory and in the calculus of constructions. Our analysis is presented as a form of abstract interpretation that allows a wider syntactic class of corecursive definitions to be recognised as productive than in previous work. Thus programmers will have fewer restrictions on their use of infinite streams within a strongly normalizing functional language.