Functional database query languages as typed lambda calculi of fixed order (extended abstract)
Functional database query languages as typed lambda calculi of fixed order (extended abstract)
复制标题
函数式数据库查询语言作为固定顺序的类型化 lambda 演算（扩展抽象）
DOI：
--
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
P. Kanellakis
中科院分区：
文献类型：
--
作者：
Gerd G. Hillebrand;P. Kanellakis
我们提出了一个数据库查询语言的功能框架，它类似于有限结构上的一阶和固定点公式的传统逻辑框架。我们使用0阶原子常量，这些常量、变量、应用程序、lambda抽象和let抽象之间的相等性；全部使用固定顺序 (≤ 5) 功能键入。在这个框架中，[21]中提出了任意顺序功能，查询和数据库都是类型化的 lambda 项，评估是通过归约，主要的编程技术是列表迭代。我们定义了两个语言家族：TLI=i 或 i+3 阶的简单类型列表迭代，且具有相等性；MLI=i 或 i+3 阶的 ML 类型列表迭代，具有相等性；我们使用 i+3，因为我们的数据库列表表示至少需要 3 阶。我们证明： FO 查询 ⊆TLI=0 ⊆MLI=0 ⊆LOGSPACE 查询 ⊆TLI=1 =MLI=1 = PTIME 查询 ⊆ TLI2，其中相等不再是 TLI2 中的原语。我们还表明，仅限于固定顺序的 ML 类型推断是所键入程序大小的多项式。由于使用低阶功能和类型推断进行编程在函数式语言中很常见，因此我们的结果表明此类程序足以表达有效的计算，并且可以有效地推断它们的 ML 类型。
We present a functional framework for database query languages, which is analogous to the conventional logical framework of first-order and fixpoint formulas over finite structures. We use atomic constants of order 0, equality among these constants, variables, application, lambda abstraction, and let abstraction; all typed using fixed order (≤ 5) functionalities. In this framework, proposed in [21] for arbitrary order functionalities, queries and databases are both typed lambda terms, evaluation is by reduction, and the main programming technique is list iteration. We define two families of languages: TLI=i or simply-typed list iteration of order i+3 with equality, and MLI=i or ML-typed list iteration of order i+3 with equality; we use i+3 since our list representation of databases requires at least order 3. We show that: FO-queries ⊆TLI=0 ⊆MLI=0 ⊆LOGSPACE-queries ⊆TLI=1 =MLI=1 = PTIME-queries ⊆ TLI2, where equality is no longer a primitive in TLI2. We also show that ML type inference, restricted to fixed order, is polynomial in the size of the program typed. Since programming by using low order functionalities and type inference is common in functional languages, our results indicate that such programs suffice for expressing efficient computations and that their ML-types can be efficiently inferred.