Mapping constants

A function between constant domains acts on first-order syntax by replacing every constant symbol and leaving every variable untouched. This chapter defines that action on terms and formulas, proves that it respects composition, and specializes the formula map to carry parameter-free formulas, whose constant domain is the empty type, into formulas over any constant domain.

A formula such as var 0 ∈̇ con k names two things in two different ways: var 0 refers through the free variables, while con k refers through the constant domain, some type K. Now suppose we are given a function f : K → K'. What should the relabelled formula look like? The natural answer is that only the constant moves: con k becomes con (f k), while the variable, the membership relation, and the overall shape of the formula stay exactly as they were. This chapter defines that relabelling on terms and then on formulas, working with the types Term and Formula from the syntax chapter and their full stock of constructors: the atomic relations _∈̇_ and _≐_, the connectives, and the quantifiers including the bounded forms ∀̇∈ and ∃̇∈.

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.Manipulation.ConstantMapping where

open import Base.Prelude
open import FOL.Syntax using
  ( Term; con; var; Formula; _∈̇_; _≐_; _∧̇_; _∨̇_; _⇒̇_; ⊥̇; ∃̇_; ∀̇_; ∀̇∈; ∃̇∈ )

One special choice of domain will deserve its own attention: the empty type ⊥*. A formula whose constant domain is ⊥* contains no constants at all, and the end of this chapter studies how such formulas map into formulas over any K. Until then, everything takes place for an arbitrary function between constant domains.

import Cubical.Data.Empty as Empty

Syntax level

The syntax is functorial in its constant domain: a map K → K' pushes through a term or formula, relabelling constants while preserving de Bruijn variables and logical structure. This section defines that action; the composition law is proved in the next section.

On terms the action leaves no room for choice. mapTm takes the relabelling function f : K → K' and a term of free-variable arity n, and returns a term of the same arity n: the constant con k becomes con (f k) and the variable var i is returned unchanged. This is a relabelling of constant symbols only; it is not substitution and has no effect on variables.

mapTm : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}
      → (K → K') → Term K n → Term K' n
mapTm f (con k) = con (f k)
mapTm f (var i) = var i

mapFo : ∀ {ℓ ℓ'} {K : Type ℓ} {K' : Type ℓ'} {n}

An atomic formula shows how the action extends to formulas. The image of t ∈̇ u under mapFo is mapTm f t ∈̇ mapTm f u: the same relation applied to the two mapped terms, over the same arity n. So the running example var 0 ∈̇ con k maps to var 0 ∈̇ con (f k), in which only the constant has moved.

      → (K → K') → Formula K n → Formula K' n
mapFo f (t ∈̇ u)  = mapTm f t ∈̇ mapTm f u
mapFo f (t ≐ u)  = mapTm f t ≐ mapTm f u
mapFo f (φ ∧̇ ψ)  = mapFo f φ ∧̇ mapFo f ψ
mapFo f (φ ∨̇ ψ)  = mapFo f φ ∨̇ mapFo f ψ

A quantified formula shows that logical structure is untouched. Under mapFo, a quantifier prefix is kept and its body, of arity suc n, is mapped recursively and returned with the same arity; each connective is rebuilt on the mapped subformulas. The operation neither adds nor removes a binder, and no constructor ever changes shape; falsity ⊥̇, which carries no constant, maps to itself.

mapFo f (φ ⇒̇ ψ)  = mapFo f φ ⇒̇ mapFo f ψ
mapFo f ⊥̇        = ⊥̇
mapFo f (∃̇ φ)    = ∃̇ mapFo f φ
mapFo f (∀̇ φ)    = ∀̇ mapFo f φ
mapFo f (∀̇∈ t φ) = ∀̇∈ (mapTm f t) (mapFo f φ)

The bounded quantifiers ∀̇∈ and ∃̇∈ are the case where both operations meet, since they combine a term with a formula: the bounding term t is relabelled by mapTm and the body by mapFo. With this, mapFo transforms syntax only; it never interprets a formula or touches an environment.

mapFo f (∃̇∈ t φ) = ∃̇∈ (mapTm f t) (mapFo f φ)

Two such maps in a row are one map: mapping by f and then by g agrees, as a path, with mapping once by λ k → g (f k). This functoriality of the constant-domain action is what later chapters use to collapse an intermediate constant domain, and it belongs to the syntax level rather than to any one application.

The composition law is a commuting square. If a term is mapped first along f : K → K' and then along g : K' → K'', the result should agree with mapping it once along the composite λ k → g (f k). mapTm-comp states exactly this, as a path in Term K'' n. On a constant, both sides compute to con (g (f k)), so the agreement already holds as definitional equality and refl proves the case; on a variable no constant occurs, so the two sides are again the same term.

mapTm-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (t : Term K n)
           → mapTm g (mapTm f t) ≡ mapTm (λ k → g (f k)) t
mapTm-comp f g (con k) = refl
mapTm-comp f g (var i) = refl

For formulas the same square is stated by mapFo-comp: the two routes around the square, mapFo g (mapFo f φ) and mapFo (λ k → g (f k)) φ, are paths of the same type Formula K'' n. Since the square is already proved for terms, the atomic cases need no new argument on terms: congruence cong₂ lifts the two term paths into a path between the rebuilt atoms.

mapFo-comp : ∀ {ℓ ℓ' ℓ''} {K : Type ℓ} {K' : Type ℓ'} {K'' : Type ℓ''} {n}
             (f : K → K') (g : K' → K'') (φ : Formula K n)
           → mapFo g (mapFo f φ) ≡ mapFo (λ k → g (f k)) φ
mapFo-comp f g (t ∈̇ u)  = cong₂ _∈̇_ (mapTm-comp f g t) (mapTm-comp f g u)
mapFo-comp f g (t ≐ u)  = cong₂ _≐_ (mapTm-comp f g t) (mapTm-comp f g u)

Structural recursion propagates the square through the connectives: each subformula carries its own instance, and congruence rebuilds the connective on the two subformula paths. Falsity ⊥̇ contains neither constants nor subformulas, so both routes compute to the same formula and the case is refl.

mapFo-comp f g (φ ∧̇ ψ)  = cong₂ _∧̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ∨̇ ψ)  = cong₂ _∨̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g (φ ⇒̇ ψ)  = cong₂ _⇒̇_ (mapFo-comp f g φ) (mapFo-comp f g ψ)
mapFo-comp f g ⊥̇        = refl
mapFo-comp f g (∃̇ φ)    = cong ∃̇_ (mapFo-comp f g φ)

The quantifier cases close the induction: a prefix quantifier applies to one subformula, while the bounded forms ∀̇∈ and ∃̇∈ pair a term with a body and use both the term path and the body path. Since every constructor of Formula is covered, the composition square commutes for every formula. This functoriality is a purely syntactic fact, available wherever later chapters need to collapse an intermediate constant domain.

mapFo-comp f g (∀̇ φ)    = cong ∀̇_ (mapFo-comp f g φ)
mapFo-comp f g (∀̇∈ t φ) = cong₂ ∀̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)
mapFo-comp f g (∃̇∈ t φ) = cong₂ ∃̇∈ (mapTm-comp f g t) (mapFo-comp f g φ)

The most frequently used instance of the map enters a constant domain from no constants. The syntax chapter introduced the parameter-free formulas, whose constant domain is the empty type; like sentences they have no separate name, and the type Formula (⊥* {ℓ}) n expresses the full definition: a formula of this type contains no constant nodes at all, but may still use any of its n available free-variable slots. Relabelling into a type K requires a function ⊥* → K, and the empty type is exactly the type for which such a function exists uniquely, with no case to define: there is no constant to send anywhere. This is what the eliminator Empty.rec* provides, and relabelling along it maps parameter-free formulas into formulas over any domain.

embed is exactly mapFo Empty.rec*: the unique function ⊥* → K from the empty constant alphabet is used as the relabelling, so every constant position, of which there are none, is sent somewhere. What changes is the constant domain alone: the free-variable context of length n and the binders are untouched, so embed neither closes the formula nor supplies an environment for its variables.

embed : ∀ {ℓ ℓ'} {K : Type ℓ'} {n} → Formula (⊥* {ℓ}) n → Formula K n
embed = mapFo Empty.rec*

Recap

mapTm and mapFo express the syntax-level action of a map of constant domains: constants are relabelled, variables, binders and arities are untouched. mapFo-comp proves this action is functorial under composition, and embed is the parameter-free instance, the basis for later constant relabelling and parameter abstraction.