6
$\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?

New contributor
Manuel Jacob is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
  • $\begingroup$ In fact I learned first about skolemization when programming in Haskell with existential types. $\endgroup$ – Turion Aug 15 at 7:04
5
$\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

Manuel Jacob is a new contributor. Be nice, and check out our Code of Conduct.

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.