Interpretação teórica do tipo de Skolemization

Qual é a interpretação teórica do tipo / equivalente de Skolemization?

A skolemization converte alguma fórmula na forma normal da Skolem. As duas fórmulas são satisfatórias entre si.

Ou, para dizer em termos teóricos do tipo: Existe um programa com algum tipo, se houver um programa com esse tipo na forma normal do Skolem.

Como esses programas se relacionam?

A skolemization corresponde ao chamado axioma teórico de escolha do tipo, que é brevemente discutido na seção 1.6 do livro HoTT .

$\Sigma$$\Pi$$A : U$$B : A \to U$$C : \prod_{a : A} B\,a \to U$

$$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)$$

A prova disso é muito simples, por exemplo, no Agda, temos o seguinte (provando isomorfismo em vez de equivalência por simplicidade agora):

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)

$\Sigma$

De uma perspectiva mais operacional, isso corresponde ao levantamento lambda , uma transformação de programa usada em compiladores, que eleva as definições em um escopo externo, adicionando parâmetros de função extras para variáveis ​​ligadas.