« Home

Pattern Unification 演算法理論部分 [F6C1]

在這篇文章裡面我想要探討 Elaboration Zoo 裡面的 pattern unification 演算法怎麼算出來的，以及在什麼時候成立。主要是了解我們怎麼導出等式：

?α=?rhs′[spm−1] ?\alpha \overset{?}{=} \text{rhs}'[sp_m^{-1}]

超越 Elaboration zoo 中的合一演算法與隱式參數 僅是直覺的推理。在 Display map category 我們已經了解到，contexts 跟 substitutions 構成了一個範疇，而我們想要知道的是 epimorphism 的定義，所以 Kovacs 的第一步是把 epimorphism 定義改寫成更適合這個案例的定義

Definition. Epimorphism [local-0]

我們說 Sub Γ ΔSub\ \Gamma\ \Delta 是 epimorphism iff

δ∘σ=δ′∘σ⇒δ=δ′A[σ]=A′[σ]⇒A=A′\begin{aligned} \delta \circ \sigma = \delta' \circ \sigma \Rightarrow \delta = \delta' \\ A[\sigma] = A'[\sigma] \Rightarrow A = A' \end{aligned}

這也導出了 term 的事實：u[σ]=u′[σ]⇒u=u′u[\sigma] = u'[\sigma] \Rightarrow u = u'

我們關心一個 substitutions 中的子集：renamings

Definition. Renamings [local-1]

一個 substitution σ:Sub Γ Δ\sigma : Sub\ \Gamma\ \Delta 如果純粹由變數構成，那麼它是 renaming，記成 σ:Ren Γ Δ\sigma : Ren\ \Gamma\ \Delta

而且 Renaming 有以下特性

  1. 如果只用到 Γ\Gamma 中的變數至多一次，那麼 σ\sigma 是 epimorphism
  2. 如果只用到 Γ\Gamma 中的變數至少一次，那麼 σ\sigma 是 monomorphism
  3. 如果只用到 Γ\Gamma 中的變數剛好一次，那麼 σ\sigma 是 isomorphism（context 的 permutation）

Definition. Embeddings [local-2]

Renamings 還有一個子集叫 Embeddings，是 Δ\Delta 為 Γ\Gamma 捨棄 0 到多個變數後組成的 context。

  1. 每個 embedding 都是 epimorphism
  2. embedding Γ→Γ\Gamma \to \Gamma 一定是 identity

Renaming σ\sigma 總是能被分解為（這個動作叫 strengthening，可以延伸到 type/term 的 substitution 上）

σm∘σe=σ\sigma_m \circ \sigma_e = \sigma

其中 σm\sigma_m 是一個 monomorphism，而 σe\sigma_e 是一個 embedding

Pattern unification 問題是，在某個 context Γ\Gamma 下有等式

Γ⊢?α[sp]=?rhs \Gamma \vdash ?\alpha [sp] \overset{?}{=} \text{rhs}

其中

  • Δ⊢?α:A\Delta \vdash ?\alpha : A
  • sp:Sub Γ Δsp : Sub\ \Gamma\ \Delta
  • Γ⊢rhs:A[sp]\Gamma \vdash \text{rhs} : A[sp]

所謂的 pattern conditions 是以下 3 個條件

  1. spsp 是一個 epimorphism 跟 renaming，可以分解成 spm∘spesp_m \circ sp_e
  2. rhs=rhs′[spe]\text{rhs} = \text{rhs}'[sp_e]
  3. α\alpha 這個 meta variable 在 rhs\text{rhs} 中不是自由變數

spsp 是 epimorphism 意味著 spmsp_m 也是 epimorphism，因此 spmsp_m 是 isomorphism，具有 inverse spm−1sp_m^{-1}。從初始問題出發

?α[sp]=?rhs ?\alpha [sp] \overset{?}{=} \text{rhs}

分解 spsp 得到

?α[spm∘spe]=?rhs ?\alpha [sp_m \circ sp_e] \overset{?}{=} \text{rhs}

替換 rhsrhs 得到

?α[spm][spe]=?α[spm∘spe]=?rhs′[spe] ?\alpha [sp_m][sp_e] = ?\alpha [sp_m \circ sp_e] \overset{?}{=} \text{rhs}'[sp_e]

embedding 是 epimorphism

?α[spm]=?rhs′ ?\alpha [sp_m] \overset{?}{=} \text{rhs}'

套上 spm−1sp_m^{-1}

?α[spm∘spm−1]=?α[spm][spm−1]=?rhs′[spm−1] ?\alpha [sp_m \circ sp_m^{-1}] = ?\alpha [sp_m][sp_m^{-1}] \overset{?}{=} \text{rhs}'[sp_m^{-1}]

inverse 對消

?α=?rhs′[spm−1] ?\alpha \overset{?}{=} \text{rhs}'[sp_m^{-1}]

這促使我們定義 ?α:=rhs′[spm−1]?\alpha := \text{rhs}'[sp_m^{-1}]，然後就只需要檢查 ?α?\alpha 不是解的自由變量就可以了，原因參考 Elaboration with first-class implicit function types 的細節。直覺一點來說，本來的假定條件會導出 α\alpha 不是自由的，如果檢查卻發現它是自由的，就表示假定條件不成立。

最後

  1. 判斷 Renaming 是不是 epimorphism
  2. 分解 Renaming
  3. type/term 的 strengthening（如果 type theory 是 normalizing）

這三個演算法都是可判定的，因此 pattern unification 這個演算法是可判定的。而且由於分解唯一，解也是唯一的。