查看“︁逻辑框架”︁的源代码

{{expand english|time=2021-08-06T07:44:24+00:00}}
在[[类型论]]中，'''LF 逻辑框架'''提供了定义(或表示)逻辑的一种方式。它基于了通过有[[依赖类型]]的[[lambda 演算]]方式的对语法、规则和证明的一般性处理。语法按类似于但更一般性的 [[Per Martin-Löf]] 文章中的系统的风格来处理。

要描述一个逻辑框架，你必须提供如下:

1. 对要表示的那一类对象-逻辑的特征描述；

2. 适当的元-语言；

3. 对表示对象-逻辑的机制的特征描述。

总结为:

:“框架 = 语言 + 表示”。

在 '''LF 逻辑框架'''的情况下，这个语言是 <math>\lambda\Pi</math>-演算。这是与对一阶极小逻辑的[[命题为类型原理]]有关的一阶依赖函数类型的一个系统。<math>\lambda\Pi</math>-演算的关键特征是它由三层的实体组成: 对象、类型和类型家族。它是[[直谓性]]的，所有良好类型的项都是[[强规范化]]的和有 [[Church-Rosser定理]]性质的，是强类型的性质是[[可判定性]]的。但是[[类型推论]]是[[不可判定性]]的。

逻辑在 '''LF 逻辑框架'''中通过判断为类型编码来表示。这来源于 [[Per Martin-Löf]] 对[[康德]]的[[判断]]的概念的发展。两个高阶判断，假言的 <math>J\vdash K</math> 和一般的 <math>\Lambda x\in J. K(x)</math>，分别对应于普通的和依赖的函数空间。判断为类型的方法论是把判断表示为它们的证明的类型。逻辑系统 <math>{\mathcal L}</math> 由把种类(kind)和类型指派到表示它的语法、它的判断和它的规则模式(scheme)的有限集合的它的标署(signature)来表示。对象-逻辑的规则和证明被看做假言-一般判断 <math>\Lambda x\in C. J(x)\vdash K</math> 的原始证明。

LF 逻辑框架在[[卡内基梅隆大学]]的 [[Twelf]] 系统中实现了。Twelf 包括
:* 逻辑编程引擎
:* 关于逻辑编程(终止，覆盖等)的元理论推理
:* 归纳法[[元逻辑]]定理证明器

== 引用 ==

* [[Robert Harper (computer scientist)|Robert Harper]], Furio Honsell and [[Gordon Plotkin]]. ''A Framework For Defining Logics''. Journal of the Association for Computing Machinery, 40(1):143-184, 1993
* Arnon Avron, Furio Honsell, Ian Mason and Randy Pollack. ''Used Typed Lambda Calculus to Implement on a Machine''. Journal of Automated Reasoning, 9:309-354, 1992.
* Robert Harper. ''An Equational Formulation of LF''. Technical Report, University of Edinburgh, 1988. LFCS report ECS-LFCS-88-67.
* Robert Harper, Donald Sannella and Andrzej Tarlecki. ''Structured Theory Presentations and Logic Representations''. Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.
* Philippa Gardner. ''Representing Logics in Type Theory''. Technical Report, University of Edinburgh, 1992. LFCS report ECS-LFCS-92-227.
* Gilles Dowek. ''The undecidability of typability in the lambda-pi-calculus''. In M. Bezem, J.F. Groote (Eds.), Typed Lambda Calculi and Applications. Volume 664 of ''Lecture Notes in Computer Science'', 139-145, 1993.

[[Category:Lambda演算]]
[[Category:类型论]]