在正確處理單位的算術系統一文中，討論過要怎麼用 type system 幫我們限制單位的正確性，在檢查的時候，我發現我沒有處理到像是
[] ＝ [(Second , 0)]
這樣的問題。除此之外，這個 List 也應該要能夠忽視順序的影響，確保
(Kilogram , negsucc 0) ∷ (Second , negsucc 0) ∷ [] ＝ (Second , negsucc 0) ∷ (Kilogram , negsucc 0) ∷ []
的成立。就根本來說，原因是因為 List (Unit × ℤ) 並不是我們想表示的代數的正確 model，使得一個值具有多個表達方式。確保一個值只有一個表達方式，是一種正規形式問題。因此這裡我想討論數個可能的修正方案，並觀察他們的差異與優劣
對 List 取 quotient [ag-YGG9]
{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan hiding (_+_) open import MLTT.List open import MGS.MLTT using (has-decidable-equality) open import UF.FunExt open import UF.Base using (ap₂; happly) open import UF.Subsingletons open import UF.Subsingletons-FunExt open import UF.Sets open import UF.Sets-Properties open import Quotient.Type open import Integers.Type open import Integers.Addition open import Integers.Negation module ag-YGG9 (fe : Fun-Ext) (sq : general-set-quotients-exist (λ 𝓥 → 𝓥)) where open general-set-quotients-exist sq data Unit : 𝓤₀ ̇ where Meter Kilogram Second : Unit Unit-≟ : has-decidable-equality Unit Unit-≟ Meter Meter = inl refl Unit-≟ Kilogram Kilogram = inl refl Unit-≟ Second Second = inl refl Unit-≟ Meter Kilogram = inr λ () Unit-≟ Meter Second = inr λ () Unit-≟ Kilogram Meter = inr λ () Unit-≟ Kilogram Second = inr λ () Unit-≟ Second Meter = inr λ () Unit-≟ Second Kilogram = inr λ ()
最直覺的想法是繼續用 List (Unit × ℤ) 為 raw
representation，但需要定義等價類取 quotient
去掉那些我們不想要的情況。為此我們需要定義指數在所有單位相同來決定的等價關係
exp : Unit → List (Unit × ℤ) → ℤ exp u [] = pos 0 exp u ((v , n) ∷ xs) with Unit-≟ u v ... | inl _ = n + exp u xs ... | inr _ = exp u xs
us₁ ≈ us₂ 若且唯若 exp u us₁ = exp u us₂
對所有 u 成立
_≈_ : List (Unit × ℤ) → List (Unit × ℤ) → 𝓤₀ ̇ us₁ ≈ us₂ = (u : Unit) → exp u us₁ ＝ exp u us₂ ≈-prop : is-prop-valued _≈_ ≈-prop us₁ us₂ = Π-is-prop fe (λ u → ℤ-is-set) ≈-refl : reflexive _≈_ ≈-refl us u = refl ≈-sym : symmetric _≈_ ≈-sym us vs h u = (h u) ⁻¹ ≈-trans : transitive _≈_ ≈-trans us vs ws h k u = h u ∙ k u ≋ : EqRel (List (Unit × ℤ)) ≋ = _≈_ , ≈-prop , ≈-refl , ≈-sym , ≈-trans Units : 𝓤₀ ̇ Units = List (Unit × ℤ) / ≋
這邊證明了單位 u 在兩個 List 中的指數相加跟對 concat
起來的 List 計算 u 的指數一定是同一個數字
exp-++ : (u : Unit) (xs ys : List (Unit × ℤ)) → exp u (xs ++ ys) ＝ exp u xs + exp u ys exp-++ u [] ys = ℤ-zero-left-neutral (exp u ys) ⁻¹ exp-++ u ((v , n) ∷ xs) ys with Unit-≟ u v ... | inl _ = ap (n +_) (exp-++ u xs ys) ∙ ℤ+-assoc n (exp u xs) (exp u ys) ⁻¹ ... | inr _ = exp-++ u xs ys
再來證明 concat 是遵守 ≈ 關係的
++-resp : {us₁ us₁' us₂ us₂' : List (Unit × ℤ)} → us₁ ≈ us₁' → us₂ ≈ us₂' → (us₁ ++ us₂) ≈ (us₁' ++ us₂') ++-resp {us₁} {us₁'} {us₂} {us₂'} h k u = exp u (us₁ ++ us₂) ＝⟨ exp-++ u us₁ us₂ ⟩ exp u us₁ + exp u us₂ ＝⟨ ap₂ _+_ (h u) (k u) ⟩ exp u us₁' + exp u us₂' ＝⟨ exp-++ u us₁' us₂' ⁻¹ ⟩ exp u (us₁' ++ us₂') ∎
這邊定義一個 helper，實現 raw representation 乘上 Units
得到 Units
的運算，這可以幫助我們簡化等一下要定義的完整單位乘法
*-unit-r : List (Unit × ℤ) → Units → Units *-unit-r xs = mediating-map/ ≋ (/-is-set ≋) (λ ys → η/ ≋ (xs ++ ys)) (λ {ys} {ys'} k → η/-identifies-related-points ≋ (++-resp {xs} {xs} (≈-refl xs) k))
定義最後的單位乘法
*-unit : Units → Units → Units *-unit = mediating-map/ ≋ (Π-is-set fe (λ _ → /-is-set ≋)) *-unit-r λ {xs} {xs'} h → dfunext fe (λ q → resp-left q h) where resp-left : (q : Units) {xs xs' : List (Unit × ℤ)} → xs ≈ xs' → *-unit-r xs q ＝ *-unit-r xs' q resp-left q {xs} {xs'} h = /-induction ≋ (λ q → /-is-set ≋ {*-unit-r xs q} {*-unit-r xs' q}) on-list q where on-list : (ys : List (Unit × ℤ)) → *-unit-r xs (η/ ≋ ys) ＝ *-unit-r xs' (η/ ≋ ys) on-list ys = *-unit-r xs (η/ ≋ ys) ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⟩ η/ ≋ (xs ++ ys) ＝⟨ η/-identifies-related-points ≋ (++-resp {xs} {xs'} {ys} {ys} h (≈-refl ys)) ⟩ η/ ≋ (xs' ++ ys) ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⁻¹ ⟩ *-unit-r xs' (η/ ≋ ys) ∎
我們構造一些案例
1m : Units 1m = η/ ≋ ((Meter , pos 1) ∷ []) 1s : Units 1s = η/ ≋ ((Second , pos 1) ∷ []) 1/s : Units 1/s = η/ ≋ ((Second , negsucc 0) ∷ [])
這裏證明了純量 1 確實是單位乘法的 identity
ε : Units ε = η/ ≋ [] *-unit-η : (xs ys : List (Unit × ℤ)) → *-unit (η/ ≋ xs) (η/ ≋ ys) ＝ η/ ≋ (xs ++ ys) *-unit-η xs ys = *-unit (η/ ≋ xs) (η/ ≋ ys) ＝⟨ happly (universality-triangle/ ≋ (Π-is-set fe (λ _ → /-is-set ≋)) _ _ xs) (η/ ≋ ys) ⟩ *-unit-r xs (η/ ≋ ys) ＝⟨ universality-triangle/ ≋ (/-is-set ≋) _ _ ys ⟩ η/ ≋ (xs ++ ys) ∎ ε-is-unit-of-* : (xs : List (Unit × ℤ)) → *-unit ε (η/ ≋ xs) ＝ *-unit (η/ ≋ xs) ε ε-is-unit-of-* xs = *-unit ε (η/ ≋ xs) ＝⟨ *-unit-η [] xs ⟩ η/ ≋ ([] ++ xs) ＝⟨ ap (λ - → η/ ≋ -) ([]-right-neutral xs) ⟩ η/ ≋ (xs ++ []) ＝⟨ *-unit-η xs [] ⁻¹ ⟩ *-unit (η/ ≋ xs) ε ∎
單位取消確實如想像中一樣運作
cancel : *-unit 1s 1/s ＝ ε cancel = *-unit 1s 1/s ＝⟨ *-unit-η _ _ ⟩ η/ ≋ (((Second , pos 1) ∷ []) ++ ((Second , negsucc 0) ∷ [])) ＝⟨ η/-identifies-related-points ≋ I ⟩ η/ ≋ [] ∎ where I : ((Second , pos 1) ∷ (Second , negsucc 0) ∷ []) ≈ [] I Meter = refl I Kilogram = refl I Second = refl
不同單位確實有被等價類分開
different-units : (u₁ u₂ : Unit) → ¬ (u₁ ＝ u₂) → ¬ (((u₁ , pos 1) ∷ []) ≈ ((u₂ , pos 1) ∷ [])) different-units Meter Meter ne h = ne refl different-units Meter Kilogram ne h = pos-succ-not-zero 0 (h Meter) different-units Meter Second ne h = pos-succ-not-zero 0 (h Meter) different-units Kilogram Meter ne h = pos-succ-not-zero 0 (h Kilogram) different-units Kilogram Kilogram ne h = ne refl different-units Kilogram Second ne h = pos-succ-not-zero 0 (h Kilogram) different-units Second Meter ne h = pos-succ-not-zero 0 (h Second) different-units Second Kilogram ne h = pos-succ-not-zero 0 (h Second) different-units Second Second ne h = ne refl
不過這個方法雖然概念上很直觀，但就如同你直接看到的，寫起來非常複雜。
從構造就拒絕錯誤 [ag-SPBG]
{-# OPTIONS --safe --without-K #-} open import MLTT.Spartan hiding (_+_) open import MLTT.Maybe open import MGS.MLTT using (has-decidable-equality) open import Integers.Type open import Integers.Addition module ag-SPBG where data Unit : 𝓤₀ ̇ where Meter Kilogram Second : Unit Unit-≟ : has-decidable-equality Unit Unit-≟ Meter Meter = inl refl Unit-≟ Kilogram Kilogram = inl refl Unit-≟ Second Second = inl refl Unit-≟ Meter Kilogram = inr λ () Unit-≟ Meter Second = inr λ () Unit-≟ Kilogram Meter = inr λ () Unit-≟ Kilogram Second = inr λ () Unit-≟ Second Meter = inr λ () Unit-≟ Second Kilogram = inr λ ()
為了讓構造出來的 List
裡面的單位只有一種正確排列方式，我們可以幫單位附上順序，這個順序其實並不重要，只是需要有一個來確保
List
只有一種排列方法，從而去除因為排列順序不同而無法被定義等價認出來的不同表達方式（[A, B]
跟 [B, A] 兩種構造）
_<Unit_ : Unit → Unit → 𝓤₀ ̇ Meter <Unit Meter = 𝟘 Meter <Unit Kilogram = 𝟙 Meter <Unit Second = 𝟙 Kilogram <Unit Meter = 𝟘 Kilogram <Unit Kilogram = 𝟘 Kilogram <Unit Second = 𝟙 Second <Unit _ = 𝟘 <Unit-trans : (u v w : Unit) → u <Unit v → v <Unit w → u <Unit w <Unit-trans Meter Kilogram Second _ _ = ⋆ <Unit-trans Meter Kilogram Kilogram _ () <Unit-trans Meter Kilogram Meter _ () <Unit-trans Meter Second _ _ () <Unit-trans Kilogram Second _ _ () <Unit-trans Meter Meter _ () _ <Unit-trans Kilogram Meter _ () _ <Unit-trans Kilogram Kilogram _ () _ <Unit-trans Second _ _ () _ data Tri (u v : Unit) : 𝓤₀ ̇ where is-< : u <Unit v → Tri u v is-≡ : u ＝ v → Tri u v is-> : v <Unit u → Tri u v tri : (u v : Unit) → Tri u v tri Meter Meter = is-≡ refl tri Meter Kilogram = is-< ⋆ tri Meter Second = is-< ⋆ tri Kilogram Meter = is-> ⋆ tri Kilogram Kilogram = is-≡ refl tri Kilogram Second = is-< ⋆ tri Second Meter = is-> ⋆ tri Second Kilogram = is-> ⋆ tri Second Second = is-≡ refl
單位定了順序之後，這裏規定 List 中的單位必須按照特定順序排列，確保每個組合單位的表示形式只有一種
data _<?_ : Maybe Unit → Unit → 𝓤₀ ̇ where no-bd : ∀ {u} → Nothing <? u bd : ∀ {v u} → v <Unit u → Just v <? u
接著在 cons 中我們規定 ¬ (n ＝ pos 0)
因此不會出現 3 s⁰ 這種可以直接寫成 3
的情況
data UL (lb : Maybe Unit) : 𝓤₀ ̇ where [] : UL lb cons : (u : Unit) → lb <? u → (n : ℤ) → ¬ (n ＝ pos 0) → UL (Just u) → UL lb Units : 𝓤₀ ̇ Units = UL Nothing <?-trans : ∀ {lb u v} → lb <? u → u <Unit v → lb <? v <?-trans no-bd _ = no-bd <?-trans (bd w<u) u<v = bd (<Unit-trans _ _ _ w<u u<v) weaken : ∀ {lb u} → lb <? u → UL (Just u) → UL lb weaken bd' [] = [] weaken bd' (cons v (bd u<v) n nz rest) = cons v (<?-trans bd' u<v) n nz rest insert : ∀ {lb} (u : Unit) → lb <? u → (n : ℤ) → ¬ (n ＝ pos 0) → UL lb → UL lb insert u ord n nz [] = cons u ord n nz [] insert u ord n nz (cons v ord' m nz' rest) with tri u v ... | is-< u<v = cons u ord n nz (cons v (bd u<v) m nz' rest) ... | is-> v<u = cons v ord' m nz' (insert u (bd v<u) n nz rest) ... | is-≡ refl with ℤ-is-discrete (n + m) (pos 0) ... | inl _ = weaken ord rest ... | inr nz-sum = cons u ord (n + m) nz-sum rest *-unit : ∀ {lb} → UL lb → Units → Units *-unit [] ys = ys *-unit (cons u _ n nz rest) ys = insert u no-bd n nz (*-unit rest ys)
構造一些案例來看看這種實現
1m : Units 1m = cons Meter no-bd (pos 1) (λ ()) [] 1s : Units 1s = cons Second no-bd (pos 1) (λ ()) [] 1/s : Units 1/s = cons Second no-bd (negsucc 0) (λ ()) []
對消就會得到純量
cancel : *-unit 1s 1/s ＝ [] cancel = refl
另外也嘗試證明比較複雜的案例
m³ : Units m³ = cons Meter no-bd (pos 3) (λ ()) [] 1m³s : Units 1m³s = cons Meter no-bd (pos 3) (λ ()) (cons Second (bd ⋆) (pos 1) (λ ()) []) m³-×̇-1s : *-unit m³ 1s ＝ 1m³s m³-×̇-1s = refl
這個方法的缺點是我們被迫仔細的構造構造子，構造複雜也難用，並創造了一個內容無關緊要的 strict order 與大量的輔助函數來處理這些問題。但比起另外兩個方案，這個方案並不需要 function extensionality，並且證明可以仰賴定義等價。
用函數表示 [ag-FKSF]
{-# OPTIONS --safe --without-K --no-exact-split #-} open import MLTT.Spartan hiding (_+_) open import UF.FunExt open import Integers.Type open import Integers.Addition open import Integers.Negation module ag-FKSF (fe : Fun-Ext) where data Unit : 𝓤₀ ̇ where Meter Kilogram Second : Unit
這裏把組合單位定義成一個函數 u：今天問
u Meter 就會知道公尺這個單位的次方是多少
UL : (X : 𝓤 ̇ ) → 𝓤 ̇ UL X = X → ℤ Units : 𝓤₀ ̇ Units = UL Unit
這個定義的好處之一是沒有單位的定義非常簡單：
ε-unit : Units ε-unit _ = pos 0
單位相乘只需要把自己的指數相加即可
*-unit : Units → Units → Units *-unit us₁ us₂ u = us₁ u + us₂ u
要取單位的乘法反元素可以定義成加法反元素
⁻¹-unit : Units → Units ⁻¹-unit us u = - us u
也就是說，我們根本就是借用了 ℤ
的代數來用，從而大幅簡化了定義。我們可以構造一些範例來看看
1m : Units 1m Meter = pos 1 1m _ = pos 0 1s : Units 1s Second = pos 1 1s _ = pos 0 m³ : Units m³ Meter = pos 3 m³ _ = pos 0 1/s : Units 1/s = ⁻¹-unit 1s
證明這確實有用
cancel-pointwise : *-unit 1s 1/s ＝ ε-unit cancel-pointwise = dfunext fe I where I : (u : Unit) → *-unit 1s 1/s u ＝ ε-unit u I Meter = refl I Kilogram = refl I Second = refl 1m³s : Units 1m³s Meter = pos 3 1m³s Second = pos 1 1m³s _ = pos 0 m³-×̇-1s : *-unit m³ 1s ＝ 1m³s m³-×̇-1s = dfunext fe I where I : (u : Unit) → *-unit m³ 1s u ＝ 1m³s u I Meter = refl I Kilogram = refl I Second = refl
這個方案的好處是他構造寫起來最直覺，在概念上很漂亮（對函數詢問特定單位的指數次方是多少），但證明的複雜性跟 quotient 版本相當。
結語 [local-0]
對所有我們能夠想到儲存方式，但表示方式具有歧意的狀況，都可以用類似的方案解決。但方案三這種直接去找理想的 model 的做法不一定能成功，混用三種方案也是有可能的，熟悉理論的多種模型會對避免粗暴的使用方案一有很大的幫助。