NuPRL り的证明 5 -- 我们来看看 Cedille

虽然说是看看 cedille, 不过主要是因为用 cedille 写这篇內容会比较方便了。这篇主要介紹的是 MLTT 70, 又被稱為 Type : Type，只要用 dependent function type 就可以 encode higher order logic。

首先就是 well known 的 dependent function type 对应 universal qualifier。之前的 LdBeth：NuPRL 中的证明–从一到CTT 中提到的 indexed family of intersection type 也对应 universal qualifier ，不过生成的 witness 会不同。在 Cedille 中 indexed intersection 用 $\forall$ ，dependent function 用 $\Pi$ 表示。

Conjunction 可以表为如下，★ ➔ ★ ➔ ★ 是 kind， $\forall P.(A \rightarrow B \rightarrow P)\rightarrow P$ 意为对任意命題 $P$ 在有 $A \rightarrow B \rightarrow P$ 时 $A \wedge B$ 可以证明 $P$ 。

Conj ◂ ★ ➔ ★ ➔ ★ = λ A: ★. λ B: ★. ∀ P: ★. (A ➔ B ➔ P) ➔ P.

而类型为 $A\rightarrow B \rightarrow A \wedge B$ 的 operator 在 NuPRL 中叫做 pair，又称作 $\wedge \negthickspace -\negthickspace \it introduction$ 在 Cedille 可实现为

pair ◂ ∀ A: ★. ∀ B: ★. A ➔ B ➔ Conj ·A ·B
= Λ A. Λ B. λ a. λ b. Λ P. λ f. f a b.

看似很复杂，但用 Cedille 的 type erase 简化以后就是 $\lambda a . \lambda b . \lambda f . (f a) b$

fst 和 snd 很自然可以定义出来：

fst ◂ ∀ A: ★. ∀ B: ★. Conj ·A ·B ➔ A
= Λ A. Λ B. λ p. p ·A (λ a. λ b. a).

snd ◂ ∀ A: ★. ∀ B: ★. Conj ·A ·B ➔ B
= Λ A. Λ B. λ p. p ·B (λ a. λ b. b).

Disjunction 则是「对任意 $P$ 在有 $(A\rightarrow P)\rightarrow (B \rightarrow P)\rightarrow P$ 时 $A \vee B$ 可证 $P$ 」

Disj ◂ ★ ➔ ★ ➔ ★ = λ A: ★. λ B: ★. ∀ P: ★. (A ➔ P) ➔ (B ➔ P) ➔ P.

它有两个 intro rule，分別是 inl 和 inr

inl ◂ ∀ A: ★. ∀ B: ★. A ➔ Disj ·A ·B
= Λ A. Λ B. λ a. Λ P. λ f. λ p. f a.

inr ◂ ∀ A: ★. ∀ B: ★. B ➔ Disj ·A ·B
= Λ A. Λ B. λ b. Λ P. λ f. λ p. p b.

而它的 elim rule，spread

spread ◂ ∀ A: ★. ∀ B: ★. ∀ P: ★. Disj ·A ·B ➔ (A ➔ P) ➔ (B ➔ P) ➔ P
= Λ A. Λ B. Λ P. λ p. λ a. λ b. p a b.

在 Cedille 中 erase 会得到 $\lambda p.p$ ，但是为什么？

还记着 Disj 的定义么？其实 spread 就是个 application。所以可以写成如下：

spread ◂ ∀ A: ★. ∀ B: ★. ∀ P: ★. Disj ·A ·B ➔ (A ➔ P) ➔ (B ➔ P) ➔ P
= Λ A. Λ B. Λ P. λ p. p ·P.

然后是 dependent product，它的 intro rule 和 conjunction 是 β-equal 的。elim rule 则同样是 application。

Sigma ◂ Π S: ★. (S ➔ ★) ➔ ★
= λ S: ★. λ A: S ➔ ★. ∀ P: ★. (Π x: S. A x ➔ P) ➔ P.

sigIntro ◂ ∀ S: ★. ∀ A: S ➔ ★. Π x: S. A x ➔ Sigma ·S ·A
=  Λ S. Λ A. λ x. λ a. Λ P. λ p. p x a.

eqPairSigIntro ◂ { pair ≃ sigIntro } = β.

sigElim ◂ ∀ S: ★. ∀ A: S ➔ ★. ∀ P: ★. Sigma ·S ·A ➔ (Π x: S. A x ➔ P) ➔ P
= Λ S. Λ A. Λ P. λ p. p ·P.

eqSElimId ◂ { sigElim ≃ λ x. x } = β.

sElim-1 ◂ ∀ S: ★. ∀ A: S ➔ ★. ∀ P: ★. Sigma ·S ·A ➔ S
= Λ S. Λ A. Λ P. λ p. sigElim ·S ·A ·S p (λ a. λ b. a).

sElim-2 ◂ ∀ S: ★. ∀ B: ★. ∀ P: ★. Sigma ·S ·(λ x: S. B) ➔ B
= Λ S. Λ B. Λ P. λ p. sigElim ·S ·(λ x: S. B) ·B p (λ a. λ b. b).

eqSigElim ◂ Conj ·{ fst ≃ sElim-1 } ·{ snd ≃ sElim-2 } = pair β β.

最后是 eq 的定义，ML70 用的是 Leibniz equality，reflection 则是个 trivial 的 identity。

Eq ◂ Π A: ★. A ➔ A ➔ ★
= λ A: ★. λ x: A. λ y: A. ∀ P: A ➔ ★. (P x) ➔ (P y).

refl ◂ ∀ A: ★. ∀ x: A. Eq ·A x x
= Λ A. Λ x: A. Λ P. λ x. x.

trans ◂ ∀ A: ★. ∀ a: A. ∀ b: A. ∀ c: A. Eq ·A a b ➔ Eq ·A b c ➔ Eq ·A a c
= Λ A. Λ a. Λ b. Λ c. λ ab. λ bc. Λ P. λ p. bc ·P (ab ·P p).

Ref

Automated Logic and Programming

https://cedille.github.io

修改：修复两处 LaTeX 渲染问题 $A \and B$ → $A \wedge B$ $A \or B$ → $A \vee B$

Ref#

Ref