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.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.