Computational aspects of the epsilon calculus

理论计算机科学中使用的许多形式主义，如数据库查询语言，规范和验证的形式主义，以及编程语言语义的类型系统，都使用非确定性选择函数。 choice函数从指定的类中非确定性地选取一个元素。 这样的形式主义可以卓有成效地调查使用逻辑结合逻辑选择操作。 希尔伯特在微积分中研究了逻辑选择算子：在微积分中，一个形式为ε-x A（x）的项是满足A（x）的某个x，如果A（x）被满足，否则是任意的。微积分和为微积分发展起来的证明论方法主要应用于数学系统的证明论分析。近年来，它也被广泛应用于计算机科学和计算语言学。例如，在Abiteboul和Vianu引入的关系数据库查询语言中，证明结构（witness construction）、抽象状态机中的选择结构（choose construction）以及可扩展软件系统中动态链接的类型基础（type foundation）中，都使用了递归运算符。

Many formalisms used in theoretical computer science such as database query languages, formalisms for specification and verification, and type systems for programming language semantics use non-deterministic choice functions. A choice function picks an element from a specified class non-deterministically. Such formalisms can be fruitfully investigated using logics incorporating a logical choice operator. Logical choice operators were investigated by Hilbert in the epsilon calculus: in the epsilon calculus, a term of the form epsilon-x A(x) is some x which satisfies A(x), if A(x) is satisfied, and arbitrary otherwise. The epsilon calculus and proof theoretic methods developed for the epsilon calculus have mainly been applied to the proof theoretic analysis of mathematical systems. In recent years, however, it has also been extensively applied in computer science and computational linguisitics. For instance, epsilon operators have been used in dealing with the witness construct in relational database query languages introduced by Abiteboul and Vianu, the choose construct in Abstract State Machines, and as a type foundation for dynamic linking in extensible software systems.