路徑誘導暗示

這是一個後續問題Getting path induction to work in Agda 路徑誘導暗示

不知何時該構造可能更有表現力。在我看來，我們總能表達同樣的，像這樣：

f : forall {A} -> {x y : A} -> x == y -> "some type" 
f refl = instance of "some type" for p == refl

這裏阿格達給予其相同c : (x : A) -> C refl從這個問題的例子會做路徑誘導：

pathInd : forall {A} -> (C : {x y : A} -> x == y -> Set) 
        -> (c : (x : A) -> C refl) 
        -> {x y : A} -> (p : x == y) -> C p

看來這功能同構於：

f' : forall {A} -> {x y : A} -> x == y -> "some type" 
f' = pathInd (\p -> "some type") (\x -> f {x} refl)

是這兩種方式（f VS pathInd）在功率相同的？

來源

2014-10-30 Sassa NF

這可能會有所幫助：http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/ – user3237465 2014-10-30 13:58:01

@ user3237465是的，我正在閱讀。然而我的問題是關於Agda爲'f'做路徑歸納。我沒有看到'pathInd'的用法，就像在HoTT中一樣被表示爲一個函數，除非它比'f'更普遍。換句話說，既然使用'pathInd'，需要複製同樣的事情來定義'f'，我沒有看到引入'pathInd'是否有任何實際的可行性，除了練習，這當然是一個優點。 – 2014-10-30 14:14:38

pathInd只是一個依賴消除器。下面是一個同構的定義：

J : ∀ {α β} {A : Set α} {x y : A} 
    -> (C : {x y : A} {p : x ≡ y} -> Set β) 
    -> ({x : A} -> C {x} {x}) 
    -> (p : x ≡ y) -> C {p = p} 
    J _ b refl = b

到這一點，你可以定義_≡_各種功能，而不模式匹配，例如：

sym : ∀ {α} {A : Set α} {x y : A} 
     -> x ≡ y 
     -> y ≡ x 
    sym = J (_ ≡ _) refl 

    trans : ∀ {α} {A : Set α} {x y z : A} 
     -> x ≡ y 
     -> y ≡ z -> x ≡ z 
    trans = J (_ ≡ _ -> _ ≡ _) id 

    cong : ∀ {α β} {A : Set α} {B : Set β} {x y : A} 
     -> (f : A -> B) 
     -> x ≡ y 
     -> f x ≡ f y 
    cong f = J (f _ ≡ f _) refl 

    subst : ∀ {α β} {A : Set α} {x y : A} 
     -> (C : A -> Set β) 
     -> x ≡ y 
     -> C x -> C y 
    subst C = J (C _ -> C _) id

但你不能從J證明身份證明的唯一性如[1]描述：

uip : ∀ {α} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q 
    uip refl refl = refl

所以你可以表達更與阿格達的模式匹配，比爲只是依賴消除。但是你可以使用--without-K選項：

{-# OPTIONS --without-K #-} 

open import Relation.Binary.PropositionalEquality 

uip : ∀ {α} {A : Set α} {x y : A} -> (p q : x ≡ y) -> p ≡ q 
uip refl refl = refl

uip現在不進行類型檢查，導致此錯誤：

Cannot eliminate reflexive equation x = x of type A because K has 
been disabled. 
when checking that the pattern refl has type x ≡ x

[1] http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/

來源

2014-10-30 15:10:47 user3237465

爲了提供一個簡短的回答：你是對，Agda的模式匹配意味着存在一個路徑感應原語。事實上，已經表明，在類型理論與宇宙，依賴性模式匹配相當於感應原語用於感應類型的存在和所謂的k-公理：

http://link.springer.com/chapter/10.1007/11780274_27

最近，它已經表明，（最新執行的）阿格達的--without-K選項限制模式匹配，使得它僅相當於用感應原語的存在了歸納類型：

http://dl.acm.org/citation.cfm?id=2628136.2628139

全面披露：我米的合着者後者的工作。

來源

2014-10-30 15:30:10

路徑誘導暗示

回答

相關問題