8
$\begingroup$

What is the type-theoretic interpretation / equivalent of Skolemization?

Skolemization converts some formula into Skolem normal form. The two formulae are equisatisfiable with each other.

Or, to say it in type-theoretic terms: There is a program having some type iff there is a program having this type in Skolem normal form.

How do these programs relate to each other?

$\endgroup$
  • $\begingroup$ In fact I learned first about skolemization when programming in Haskell with existential types. $\endgroup$ – Turion Aug 15 at 7:04
9
$\begingroup$

Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book.

This provides an equivalence along which we can swap $\Sigma$ and $\Pi$ types. Assuming $A : U$, $B : A \to U$ and $C : \prod_{a : A} B\,a \to U$, we have an equivalence:

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

The proof of this very simple, e.g. in Agda we have the following (proving isomorphism instead of equivalence for simplicity now):

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)

Going from left to right along the equivalence, we convert an existential variable into a function abstracting over the universal variable in scope. We can also use this iteratively, to move all $\Sigma$-s from a mixed-quantifier type to a prefix.

From a more operational perspective, this corresponds to lambda lifting, a program transformation used in compilers, which lifts definitions into an outer scope by adding extra function parameters for bound variables.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.