Computational aspects of the epsilon calculus

理论计算机科学中使用的许多形式化语言，如数据库查询语言、规范和验证的形式化语言，以及编程语言语义的类型系统，都使用非确定性选择函数。选择函数不确定地从指定的类中选择元素。使用包含逻辑选择运算符的逻辑可以有效地研究这种形式化。希尔伯特在微积分中研究了逻辑选择算子：在微积分中，形式为的项a (x)是某个满足a (x)的x，如果a (x)满足，否则是任意的。微积分及其发展的证明理论方法主要应用于数学系统的证明理论分析。然而，近年来，它也被广泛应用于计算机科学和计算语言学。例如，epsilon算子被用于处理Abiteboul和Vianu引入的关系数据库查询语言中的见证构造，抽象状态机中的选择构造，以及作为可扩展软件系统中动态链接的类型基础。该项目的目的是扩展在计算环境中应用的epsilon微积分以前的工作，并为它提供一个系统的基础。这包括开发和研究epsilon演算的证明理论方法，开发各种版本的epsilon演算的形式系统，研究数据库语言中作为选择函数的epsilon项的变体语义，以及研究非经典逻辑中epsilon算子的行为。特别是，直观的epsilon演算和它们的自然演绎系统将被研究：它们是编程语言语义应用的理想对象，其中类型推理演算通常反映了Curry-Howard同构下的自然演绎系统。

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.The aim of the project is to expand on previous work in applying the epsilon calculus in computational contexts and to provide a systematic foundation for it. This includes the development and investigation of proof theoretic methods for the epsilon calculus, development of formal systems for various versions of the epsilon calculus, the study of variant semantics for epsilon terms as choice functions in database languages, as well as investigating the behavior of epsilon operators in non-classical logics. In particular, intutionistic epsilon calculi and natural deduction systems for them will be studied: they are a desideratum for applications in programming language semantics, where type inference calculi typically mirror natural deduction systems under the Curry-Howard isomorphism.