邏輯框架

在類型論中，LF 邏輯框架提供了定義(或表示)邏輯的一種方式。它基於了通過有依賴類型的lambda 演算方式的對語法、規則和證明的一般性處理。語法按類似於但更一般性的 Per Martin-Löf 文章中的系統的風格來處理。

要描述一個邏輯框架，你必須提供如下:

1. 對要表示的那一類對象-邏輯的特徵描述；

2. 適當的元-語言；

3. 對表示對象-邏輯的機制的特徵描述。

總結為:

「框架 = 語言 + 表示」。

在 LF 邏輯框架的情況下，這個語言是 $\lambda \Pi$-演算。這是與對一階極小邏輯的命題為類型原理有關的一階依賴函數類型的一個系統。$\lambda \Pi$-演算的關鍵特徵是它由三層的實體組成: 對象、類型和類型家族。它是直謂性的，所有良好類型的項都是強規範化的和有 Church-Rosser定理性質的，是強類型的性質是可判定性的。但是類型推論是不可判定性的。

邏輯在 LF 邏輯框架中通過判斷為類型編碼來表示。這來源於 Per Martin-Löf 對康德的判斷的概念的發展。兩個高階判斷，假言的 $J\vdash K$ 和一般的 $\Lambda x\in J.K(x)$，分別對應於普通的和依賴的函數空間。判斷為類型的方法論是把判斷表示為它們的證明的類型。邏輯系統 ${\mathcal {L}}$ 由把種類(kind)和類型指派到表示它的語法、它的判斷和它的規則模式(scheme)的有限集合的它的標署(signature)來表示。對象-邏輯的規則和證明被看做假言-一般判斷 $\Lambda x\in C.J(x)\vdash K$ 的原始證明。

LF 邏輯框架在卡內基梅隆大學的 Twelf 系統中實現了。Twelf 包括

• 邏輯編程引擎
• 關於邏輯編程(終止，覆蓋等)的元理論推理
• 歸納法元邏輯定理證明器

引用

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