TCS Lec14总结

1. 逻辑与计算的关联

• 逻辑在计算机科学中的重要性

  • 逻辑是“计算机科学的微积分”，应用于：
    • 描述复杂性：通过逻辑描述理解计算问题的复杂度。
    • 数据库：SQL语言扩展一阶逻辑（FO）。
    • 人工智能：多智能体系统的形式化。
    • 编程语言：并发系统的程序设计与分析。

• 关键问题

  • 经典逻辑（Classical Logic）依赖排中律（$A \lor \neg A$），但直觉主义逻辑（Intuitionistic Logic） 更符合计算需求：
    • 构造性：证明 $A \lor B$ 需显式给出 $A$ 或 $B$ 的证明。
    • 经典逻辑中有效的命题（如排中律）在直觉主义中不可证。

2. 直觉主义逻辑与自然演绎

• 自然演绎系统（Gentzen, 1935）

  • 规则设计原则：每个逻辑连接词对应引入规则（Introduction Rule） 与消去规则（Elimination Rule）。
  • 和谐性（Harmony）：引入与消去规则需满足：
    • 局部可靠性（Local Soundness）：消去规则不引入额外信息（对应程序计算的规约）。
    • 局部完备性（Local Completeness）：消去规则可重构原命题（对应程序的扩展等价）。

• 逻辑连接词的规则

  逻辑符号	引入规则	消去规则
  $A \land B$	$\dfrac{A \quad B}{A \land B}$	$\dfrac{A \land B}{A}$, $\dfrac{A \land B}{B}$
  $A \supset B$	$\dfrac{[A]^x \quad \cdots \quad B}{A \supset B}$	$\dfrac{A \supset B \quad A}{B}$
  $A \lor B$	$\dfrac{A}{A \lor B}$, $\dfrac{B}{A \lor B}$	$\dfrac{A \lor B \quad [A]^x \cdots C \quad [B]^y \cdots C}{C}$
  $\bot$	无引入规则	$\dfrac{\bot}{C}$（爆炸原理）

• 直觉主义逻辑特性

  • 不可证命题：排中律（$A \lor \neg A$）、双重否定消除（$\neg \neg A \supset A$）等。
  • 吉文科定理（Gilvenko’s Theorem）：经典逻辑中 $A$ 有效 $\iff$ 直觉主义逻辑中 $\neg \neg A$ 有效。
  • 计算复杂度：直觉主义逻辑的有效性判定是PSPACE完全问题（经典逻辑为coNP完全）。

3. 命题即类型的对应（Curry-Howard Isomorphism）

• 核心对应关系

  逻辑概念	程序语言概念
  命题（Proposition）	类型（Type）
  证明（Proof）	程序（Program）
  引入规则	构造子（Constructor）
  消去规则	析构子（Destructor）
  局部规约	程序计算（$\beta$-规约）
  局部扩展	扩展等价（$\eta$-等价）

• 具体映射

  • 蕴含（$A \supset B$） → 函数类型（$A \to B$）

    • 引入规则：$\lambda x. M : A \to B$
    • 消去规则：$M N : B$（函数应用）
    • 规约：$(\lambda x.M)N \to_R M[N/x]$（$\beta$-规约）

  • 合取（$A \land B$） → 积类型（$A \times B$）

    • 构造子：$\langle M, N \rangle : A \times B$
    • 析构子：$\textsf{fst } M : A$, $\textsf{snd } M : B$
    • 规约：$\textsf{fst } \langle M,N \rangle \to_R M$

  • 析取（$A \lor B$） → 和类型（$A + B$）

    • 构造子：$\textsf{inl } M : A + B$, $\textsf{inr } N : A + B$
    • 析构子：$\textsf{case}(M, x.N, y.P) : C$
    • 规约：$\textsf{case}(\textsf{inl } M, x.N, y.P) \to_R N[M/x]$

  • 假（$\bot$） → 空类型（Void）

    • 析构子：$\textsf{abort } M : C$（无计算规则）

4. 应用与扩展

• 逻辑系统与程序语言的对应史

  逻辑系统	程序语言
  自然演绎（Gentzen, 1935）	简单类型$\lambda$-演算（Church, 1940）
  System F（Girard, 1972）	多态$\lambda$-演算（Reynolds, 1974）
  线性逻辑（Girard, 1987）	会话类型（Honda, 1993）
  模态逻辑	Monad（Moggi, 1987）

• 证明助手（Proof Assistants）

  • 基于依赖类型（Dependent Types） 扩展命题即类型（如 $\forall, \exists$）。
  • 工具：Coq（形式化数学、CompCert编译器验证）、Isabelle、Lean（自然数游戏）。