Computational aspects of the epsilon calculus

理论计算机科学中使用的许多形式化语言，如数据库查询语言、规范和验证的形式化语言，以及编程语言语义的类型系统，都使用非确定性选择函数。选择函数不确定地从指定的类中选择元素。使用包含逻辑选择运算符的逻辑可以有效地研究这种形式化。希尔伯特在微积分中研究了逻辑选择算子：在微积分中，形式为的项a (x)是某个满足a (x)的x，如果a (x)满足，否则是任意的。微积分及其发展的证明理论方法主要应用于数学系统的证明理论分析。然而，近年来，它也被广泛应用于计算机科学和计算语言学。例如，epsilon算子被用于处理Abiteboul和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.