Computational aspects of the epsilon calculus

理论计算机科学中使用的许多形式主义，例如数据库查询语言、用于规范和验证的形式主义、以及用于编程语言语义的类型系统，都使用非确定性选择函数。CHOICE函数从指定的类中非确定性地选取一个元素。可以使用包含逻辑选择运算符的逻辑来有效地研究这种形式主义。Hilbert在epsilon演算中研究了逻辑选择算子：在epsilon演算中，形式为epsilon-x的项A(X)是满足A(X)的某个x，如果A(X)满足，则任意。Epsilon演算和为epsilon演算发展的证明论方法主要应用于数学系统的证明论分析。然而，近年来，它也在计算机科学和计算语言学中得到了广泛的应用。例如，epsilon运算符已被用于处理由Abitebul和Vianu引入的关系数据库查询语言中的见证结构，抽象状态机中的选择结构，以及作为可扩展软件系统中动态链接的类型基础。

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.