Computational aspects of the epsilon calculus

点击翻译按钮获取中文摘要

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.