Interpretación teórica de tipo de Skolemization

La skolemización corresponde al llamado axioma teórico de elección, que se analiza brevemente en la sección 1.6 del libro HoTT .

Esto proporciona una equivalencia a lo largo de la cual podemos intercambiar los tipos y . Suponiendo que , y , tenemos una equivalencia: $\Sigma$ $\Pi$ $A : U$ $B : A \to U$ $C : \prod_{a : A} B\,a \to U$

una C : (\prod_{una : UNA} \sum_{si : si una} C una si) ≃ (\sum_{(si : \prod_{una : UNA} si una)} \prod_{una : UNA} C una (si una))

$ac : \Big(\prod_{a : A}\sum_{b : B\,a}\,C\,a\,b\Big) \simeq \Big(\sum_{(b : \prod_{a : A} B\,a)} \prod_{a : A} C\,a\,(b\, a)\Big)$

La prueba de esto es muy simple, por ejemplo, en Agda tenemos lo siguiente (demostrando isomorfismo en lugar de equivalencia por simplicidad ahora):

open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

iso : Set → Set → Set
iso A B =
  ∃₂ λ (f : A → B)(g : B → A) → (∀ x → f (g x) ≡ x) × (∀ x → g (f x) ≡ x)

ac : ∀ {A : Set}{B : A → Set}{C : ∀ a → B a → Set}
     → iso ((a : A) → Σ (B a) λ b → C a b)
           (Σ ((a : A) → B a) λ b → (a : A) → C a (b a))
ac = (λ f → proj₁ ∘ f , proj₂ ∘ f)
   , (λ {(b , c) a → b a , c a})
   , (λ _ → refl)
   , (λ _ → refl)

Yendo de izquierda a derecha a lo largo de la equivalencia, convertimos una variable existencial en una función que abstrae sobre el alcance de la variable universal. También podemos usar esto de forma iterativa para mover todos los -s de un tipo de cuantificador mixto a un prefijo. $\Sigma$

Desde una perspectiva más operativa, esto corresponde al levantamiento lambda , una transformación de programa utilizada en compiladores, que eleva las definiciones a un alcance externo al agregar parámetros de función adicionales para variables enlazadas.

András Kovács
fuente

Interpretación teórica de tipo de Skolemization

Respuestas: