Computational aspects of the epsilon calculus

epsilon 演算的计算方面

• 批准号: 261286-2007
• 负责人: Zach, Richard
• 金额: $ 1.02万
• 依托单位: University of Calgary
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2007
• 资助国家: 加拿大
• 起止时间: 2007-01-01 至 2008-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=363112
• 关键词: Computational; aspects; 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.

在理论计算机科学中使用的许多形式主义，如数据库查询语言，规范和验证的形式主义，编程语言语义的类型系统使用非确定性选择函数。选择函数从指定的类中选择一个元素，这样的形式主义可以使用包含逻辑选择算子的逻辑进行富有成效的研究。逻辑选择算子由希尔伯特在微积分：在微积分中，形式为ε-x A（x）的项是满足A（x）的某个x，如果A（x）被满足，否则是任意的。微积分和为微积分发展起来的证明论方法主要应用于数学系统的证明论分析。近年来，它也被广泛应用于计算机科学和计算语言学。例如，在处理Abiteboul和Vianu介绍的关系数据库查询语言中的见证结构，抽象状态机中的选择结构，作为可扩展软件系统中动态链接的类型基础。该项目的目的是扩展以前在计算环境中应用可扩展演算的工作，并为其提供系统的基础。这包括发展和调查的证明理论的方法，演算的各种版本的演算的形式系统的发展，变量语义的研究作为选择功能的数据库语言，以及调查的行为的演算运算符在非经典逻辑。特别是，直觉推理演算和自然演绎系统，他们将被研究：他们是一个必要的应用程序在编程语言语义，类型推理演算通常反映自然演绎系统下的柯里-霍华德同构。