A simple module language for LF

April 10, 2001

1 Introduction

2 Syntax and elaboration rules

Concrete syntax

decls ::= · | decl decls
decl ::= id : exp .
| id = exp : exp .
| %sig id = sigexp .
| %struct id : sigexp .
| %struct id = strexp .
| %include sigexp .
| %open strexp .

sigexp ::= id
| {decls}
| sigexp %where {insts}
strexp ::= path id
insts ::= · | inst insts
inst ::= path id := exp .
| %struct path id := strexp .
path ::= · | id . path

Elaborated syntax

Signatures  Σ ::= · | Σ, (id ▷ δ)
Declarations δ ::= c : A | c = M : A | m : Σ
Sig abbrevs Ψ ::= · | Ψ, (id = Σ)

The scoping properties of the various names that appear in a signature deserve some explanation. First we define the following notions:

dom(·) = ∅
dom(Σ, (id ▷ c : A))= dom(Σ) ∪ {c}
dom(Σ, (id ▷ c = M : A))= dom(Σ) ∪ {c}
dom(Σ, (id ▷ m : Σ_{m}))= dom(Σ) ∪ {m}∪ dom(Σ_{m})
lab(·) = ∅
lab(Σ, (id ▷ δ)) = lab(Σ) ∪ {id}

The names dom(Σ) will be referred to as the “internal” names of Σ, while the labels lab(Σ) are the “external” names. Internal names are required to be unique within a signature. Henceforward α-conversion will be used as necessary to insure that this invariant is preserved. External names, on the other hand, are only unique within the top level of the signature; external names within substructures of the signature may shadow those at higher levels. External names cannot be α-converted, because they are visible to the user.

The following rules define valid elaborated syntax:

Signature validity Σ ⊢ Σ_{1} sig

Σ ⊢ · sig

Σ ⊢ δ decl Σ, (id ▷ δ) ⊢ Σ_{1} sig
Σ ⊢ (id ▷ δ), Σ_{1} sig

Declaration validity Σ ⊢ δ decl

⊢_{Σ} A : type ; Σ ⊢ c : A decl (c ∉ dom(Σ))
⊢_{Σ} M : A

Σ ⊢ c = M : A decl

(c ∉ dom(Σ))
Σ ⊢ Σ_{m} sig ⊢ Σ_{m} uniq

Σ ⊢ m : Σ_{m} decl

(m ∉ dom(Σ))

Uniqueness of external names Σ ⊢ Σ_{1} uniq

Σ ⊢ · uniq  Σ, (id ▷ δ) ⊢ Σ_{1} uniq Σ ⊢ (id ▷ δ), Σ_{1} uniq (id ∉ lab(Σ))

Signature abbreviation context validity Σ ⊢ Ψ abbr

Σ ⊢ · abbr

Σ ⊢ Σ_{1} sig ⊢ Σ_{1} uniq Σ ⊢ Ψ abbr
Σ ⊢ (id = Σ_{1}), Ψ abbr

There is a separate judgement for signatures with unique labels because whenever sequence of definitions is collected into a structure, it is required that the labels of the components of the structure be unique. No such restriction applies to ordinary signatures, and indeed shadowing can occur between labels of a substructure and labels defined in its containing signature. The following invariants of the validity rules are all easily proved by structural induction over derivations:

1. If Σ ⊢ Σ_{1} sig and Σ, Σ_{1} ⊢ Σ_{2} sig , then Σ ⊢ Σ_{1}, Σ_{2} sig , and the converse.

2. If Σ ⊢ Σ_{1} uniq and Σ, Σ_{1} ⊢ Σ_{2} uniq , then Σ ⊢ Σ_{1}, Σ_{2} uniq , and the converse.

3. If Σ ⊢ Ψ_{1} abbr and Σ ⊢ Ψ_{2} abbr , then Σ ⊢ Ψ_{1}, Ψ_{2} abbr . The following lemmas are useful in showing certain invariants of the elaboration rules:

1. If Σ ⊢ Σ_{1} sig and Σ ⊢ Σ_{2} sig and dom(Σ_{1}) ∩ dom(Σ_{2}) = ∅, then Σ, Σ_{1} ⊢ Σ_{2} sig .

2. If Σ ⊢ Σ_{1} sig and Σ ⊢ Ψ abbr and dom(Σ_{1}) ∩ dom(Ψ) = ∅, then Σ, Σ_{1} ⊢ Ψ abbr . Here dom(Ψ) is the union of the domains of the signatures defined in Ψ.

3. If Σ_{1} ⊢ Σ_{2} uniq and lab(Σ) ∩ lab(Σ_{2}) = ∅, then Σ, Σ_{1} ⊢ Σ_{2} uniq , and the converse.

4. If Σ ⊢ Σ_{1} uniq and Σ ⊢ Σ_{2} uniq , then Σ ⊢ Σ_{1}, Σ_{2} uniq .

5. If Σ ⊢ Ψ abbr and Ψ(id) =^{α} Σ_{1} and dom(Σ_{1}) ∩ dom(Σ) = ∅, then Σ ⊢ Σ_{1} sig and ⊢ Σ_{1} uniq .

6. If ⊢ Σ sig and m ∈ dom(Σ) and Σ(m) =^{α} Σ_{m} and dom(Σ_{m}) ∩ dom(Σ) = ∅, then Σ ⊢ Σ_{m} sig and ⊢ Σ_{m} uniq .

The rules for declaration and signature elaboration use side conditions of the form (c fresh) and (Σ_{m} gen.). The former means that c is not in dom(Σ) ∪ dom(Ψ), while the latter means that dom(Σ_{m}) is disjoint from dom(Σ) ∪ dom(Ψ)—in other words, the signature Σ_{m} is “generative.” Note that in the elaboration rules for structure definitions and %open, the newly generated signature is immediately coerced to be equal to an existing signature by the signature matching judgement, so the declaration as a whole is not truly generative.

Declaration elaboration Σ; Ψ ⊢ decls ⇒ Σ_{1} Σ; Ψ ⊢ decl ⇒ Σ_{1}; Ψ_{1}

Σ; Ψ ⊢ · ⇒ ·
Σ; Ψ ⊢ decl ⇒ Σ_{1}; Ψ_{1} Σ, Σ_{1}; Ψ, Ψ_{1} ⊢ decls ⇒ Σ_{2}
Σ; Ψ ⊢ decl decls ⇒ Σ_{1}, Σ_{2}

(lab(Σ_{1}) ∩ lab(Σ_{2}) = ∅)

Σ ⊢ exp ⇒ A ⊢_{Σ} A : type

Σ; Ψ ⊢ id : exp .⇒ (id ▷ c : A); ·

(c fresh)

Σ ⊢ exp_{1} ⇒ M Σ ⊢ exp_{2} ⇒ A ⊢_{Σ} M : A
Σ; Ψ ⊢ id = exp_{1} : exp_{2} . ⇒ (id ▷ c = M : A); ·

(c fresh)

Σ; Ψ ⊢ sigexp ⇒ Σ_{1}

Σ; Ψ ⊢ %sig id = sigexp . ⇒ ·; (id = Σ_{1})

Σ; Ψ ⊢ sigexp ⇒ Σ_{m}

Σ; Ψ ⊢ %struct id : sigexp . ⇒ (id ▷ m : Σ_{m}); ·

(m fresh)

Σ ⊢ strexp ⇒ m Σ(m) =^{α} Σ_{m} Σ ⊢ m ⪯ Σ′_{m} ≤ Σ_{m}
Σ; Ψ ⊢ %struct id = strexp . ⇒ (id ▷ m_{2} : Σ′_{m}); ·

(Σ_{m} gen., m_{2} fresh)

Σ; Ψ ⊢ sigexp ⇒ Σ_{1}

Σ; Ψ ⊢ %include sigexp . ⇒ Σ_{1}; ·

Σ ⊢ strexp ⇒ m Σ(m) =^{α} Σ_{m} Σ ⊢ m ⪯ Σ′_{m} ≤ Σ_{m}
Σ; Ψ ⊢ %open strexp . ⇒ Σ′_{m}; ·

(Σ_{m} gen.)

Signature elaboration Σ; Ψ ⊢ sigexp ⇒ Σ_{1}

Ψ(id) =^{α} Σ_{1} Σ; Ψ ⊢ id ⇒ Σ_{1} (Σ_{1} gen.)

Σ; Ψ ⊢ decls ⇒ Σ_{1}
Σ; Ψ ⊢ {decls} ⇒ Σ_{1}
Σ; Ψ ⊢ sigexp ⇒ Σ_{1} Σ ⊢ insts ⇒ Σ_{1} → Σ_{2}

Σ; Ψ ⊢ sigexp %where {insts} ⇒ Σ_{2}

Structure elaboration Σ ⊢ strexp ⇒ m

Σ(id) = (m : Σ_{1})
Σ ⊢ id ⇒ m

Σ(id_{1}) = (m_{1} : Σ_{1}) Σ_{1} ⊢ path id_{2} ⇒ m

Σ ⊢ id_{1} . path id_{2} ⇒ m Instantiation elaboration Σ ⊢ insts ⇒ Σ_{1} → Σ_{2} Σ; Σ_{0} ⊢ inst ⇒ Σ_{1} → Σ_{2}

Σ ⊢ · ⇒ Σ_{1} → Σ_{1}
Σ; · ⊢ inst ⇒ Σ_{1} → Σ_{2} Σ ⊢ insts ⇒ Σ_{2} → Σ_{3}
Σ ⊢ inst insts ⇒ Σ_{1} → Σ_{3}

Σ; Σ_{0}, Σ_{1} ⊢ path id_{2} := exp . ⇒ Σ_{m} → Σ′_{m}

Σ; Σ_{0} ⊢ id_{1} . path id_{2} := exp . ⇒ Σ_{1}, (id_{1} ▷ m : Σ_{m}), Σ_{2} → Σ_{1}, (id_{1} ▷ m : Σ′_{m}), Σ_{2}

Σ; Σ_{0}, Σ_{1} ⊢ %struct path id_{2} := strexp . ⇒ Σ_{m} → Σ′_{m}

Σ; Σ_{0} ⊢ %struct id_{1} . path id_{2} := strexp . ⇒ Σ_{1}, (id_{1} ▷ m : Σ_{m}), Σ_{2} → Σ_{1}, (id_{1} ▷ m : Σ′_{m}), Σ_{2}

Σ ⊢ exp ⇒ M ⊢_{Σ,Σ_{0},Σ_{1}} M : A

Σ; Σ_{0} ⊢ id := exp . ⇒ Σ_{1}, (id ▷ c : A), Σ_{2} → Σ_{1}, (id ▷ c = M : A), Σ_{2}

Σ ⊢ exp ⇒ M_{2} ⊢_{Σ,Σ_{0},Σ_{1}} M_{1} ≡ M_{2} : A

Σ; Σ_{0} ⊢ id := exp . ⇒ Σ_{1}, (id ▷ c = M_{1} : A), Σ_{2} → Σ_{1}, (id ▷ c = M_{2} : A), Σ_{2}

Σ ⊢ strexp ⇒ m_{2} Σ, Σ_{0}, Σ_{1} ⊢ m_{2} ⪯ Σ′_{m} ≤ Σ_{m}

Σ; Σ_{0} ⊢ %struct id := strexp . ⇒ Σ_{1}, (id ▷ m_{1} : Σ_{m}), Σ_{2} → Σ_{1}, (id ▷ m_{1} : Σ′_{m}), Σ_{2}

Signature refinement  Σ ⊢ Σ_{1} ≤ Σ_{2} Σ ⊢ δ_{1} ≤ δ_{2}  (not used in elaboration)

Σ ⊢ · ≤ ·

Σ ⊢ δ_{1} ≤ δ_{2} Σ, (id ▷ δ_{1}) ⊢ Σ_{1} ≤ Σ_{2}

Σ ⊢ (id ▷ δ_{1}), Σ_{1} ≤ (id ▷ δ_{2}), Σ_{2}

⊢_{Σ} A_{1} ≡ A_{2} : type
Σ ⊢ (c : A_{1}) ≤ (c : A_{2})
⊢_{Σ} A_{1} ≡ A_{2} : type ⊢_{Σ} M_{1} : A_{1}
Σ ⊢ (c = M_{1} : A_{1}) ≤ (c : A_{2})
⊢_{Σ} A_{1} ≡ A_{2} : type ⊢_{Σ} M_{1} ≡ M_{2} : A_{1}

Σ ⊢ (c = M_{1} : A_{1}) ≤ (c = M_{2} : A_{2})

Σ ⊢ Σ_{m1} ≤ Σ_{m2}
Σ ⊢ (m : Σ_{m1}) ≤ (m : Σ_{m2})

Signature matching Σ ⊢ m ⪯ Σ_{1} ≤ Σ_{2} Σ ⊢ δ ⪯ δ_{1} ≤ δ_{2}

Σ ⊢ m ⪯ · ≤ ·
Σ(m) = Σ_{m1}, (id ▷ δ), Σ_{m2} Σ ⊢ δ ⪯ δ_{1} ≤ δ_{2} Σ, (id ▷ δ_{1}) ⊢ m ⪯ Σ_{1} ≤ Σ_{2}

Σ ⊢ m ⪯ (id ▷ δ_{1}), Σ_{1} ≤ (id ▷ δ_{2}), Σ_{2}

⊢_{Σ} A_{1} ≡ A_{2} : type
Σ ⊢ (c_{1} : A_{1}) ⪯ (c_{2} = c_{1} : A_{1}) ≤ (c_{2} : A_{2})
⊢_{Σ} A_{1} ≡ A_{2} : type
Σ ⊢ (c_{1} = M_{1} : A_{1}) ⪯ (c_{2} = c_{1} : A_{1}) ≤ (c_{2} : A_{2})
⊢_{Σ} c_{1} ≡ M_{2} : A_{1}
Σ ⊢ (c_{1} : A_{1}) ⪯ (c_{2} = c_{1} : A_{1}) ≤ (c_{2} = M_{2} : A_{2})
⊢_{Σ} c_{1} ≡ M_{2} : A_{1}
Σ ⊢ (c_{1} = M_{1} : A_{1}) ⪯ (c_{2} = c_{1} : A_{1}) ≤ (c_{2} = M_{2} : A_{2})
Σ ⊢ m_{1} ⪯ Σ_{m1} ≤ Σ_{m2}
Σ ⊢ (m_{1} : Σ_{m1}) ⪯ (m_{2} : Σ_{m1}) ≤ (m_{2} : Σ_{m2})

The following invariants of the elaboration rules are proved by mutual structural induction over derivations. Validity for declaration elaboration:

1. If ⊢ Σ sig and Σ ⊢ Ψ abbr and Σ; Ψ ⊢ decls ⇒ Σ_{1}, then Σ ⊢ Σ_{1} sig and ⊢ Σ_{1} uniq and dom(Σ_{1}) ∩ dom(Ψ) = ∅.

2. If ⊢ Σ sig and Σ ⊢ Ψ abbr and Σ; Ψ ⊢ decl ⇒ Σ_{1}; Ψ_{1}, then Σ ⊢ Σ_{1} sig and ⊢ Σ_{1} uniq and Σ, Σ_{1} ⊢

Ψ_{1} abbr and dom(Σ_{1}) ∩ dom(Ψ) = ∅. Validity for signature expression elaboration:

1. If ⊢ Σ sig and Σ ⊢ Ψ abbr and Σ; Ψ ⊢ sigexp ⇒ Σ_{1}, then Σ ⊢ Σ_{1} sig and ⊢ Σ_{1} uniq and dom(Σ_{1}) ∩

dom(Ψ) = ∅. Validity for structure expression elaboration:

1. If Σ ⊢ strexp ⇒ m, then m ∈ dom(Σ). Validity for instantiation elaboration:

1. If Σ ⊢ Σ_{1} sig and Σ ⊢ insts ⇒ Σ_{1} → Σ_{2}, then Σ ⊢ Σ_{2} ≤ Σ_{1}.

2. If Σ ⊢ Σ_{1} sig and Σ; Σ_{0} ⊢ inst ⇒ Σ_{1} → Σ_{2}, then Σ, Σ_{0} ⊢ Σ_{2} ≤ Σ_{1}. Validity for signature matching:

1. If ⊢ Σ sig and m ∈ dom(Σ) and Σ ⊢ Σ_{2} sig and Σ ⊢ m ⪯ Σ_{1} ≤ Σ_{2}, then Σ ⊢ Σ_{1} ≤ Σ_{2}. Properties of signature refinement:

1. If Σ ⊢ Σ_{2} sig and Σ ⊢ Σ_{1} ≤ Σ_{2} then Σ ⊢ Σ_{1} sig .

2. If ⊢ Σ_{2} uniq and Σ ⊢ Σ_{1} ≤ Σ_{2} then ⊢ Σ_{1} uniq .

3. If Σ ⊢ Σ_{1} ≤ Σ_{2} then dom(Σ_{1}) = dom(Σ_{2}).