Shared notation

This page defines the meta-notation reused across the other denotational-semantics pages. Read this first.

In plain terms

We use two complementary notations:

Inference rules, of the form $\frac{premises}{conclusion}$ , define a relation (typically a typing relation $Γ ⊢ e : τ$ ) inductively as the smallest relation closed under the rules.
Semantic equations, of the form $[[e]] ρ = v$ , define a function $[[\cdot]]$ by structural recursion on the syntax. The double brackets emphasise that we are speaking of meaning, not surface text.

The DSL pages in this cluster present the type system as inference rules and the value semantics as semantic equations: the standard denotational idiom, in the sense of Scott and Strachey. Where evaluation can fail to terminate, we lift the value domain $D$ to $D_{⊥} = D \cup {⊥}$ so that $[[e]]$ is total.

A context (also called an environment) is a finite map from names to data. Typing contexts map variable names to types; evaluation contexts map variable names to values; theory contexts map sort names to their definitions.

Environments

Three environment kinds appear repeatedly:

$Γ$ : a typing environment mapping variable names to types. Notation: $Γ, x : τ$ extends $Γ$ with a fresh binding $x : τ$ .
$ρ$ : a value environment mapping variable names to values. Notation: $ρ, x \mapsto v$ extends $ρ$ with $x \mapsto v$ .
$Θ$ : a theory context mapping sort names to their definitions in a GAT. Used in the theory DSL and in the pushout construction.

A judgement of the form $Γ ⊢ e : τ$ asserts that under typing context $Γ$ , the expression $e$ has type $τ$ . We do not use a separate evaluation judgement $ρ ⊢ e ⇓ v$ in this cluster: evaluation is presented as the semantic function $[[e]] ρ \in D_{⊥}$ rather than as a relation.

Inference rules

An inference rule has the form

$\frac{premises}{conclusion} (rule-name)$

Each premise and the conclusion are judgements. The rule asserts that whenever the premises hold, the conclusion follows. A derivation is a tree of rule applications whose leaves are axioms (rules with no premises) and whose root is the judgement being proved.

Semantic functions

The semantic function for a syntactic category $C$ is written $[[\cdot]]_{C} : C \to D$ where $D$ is the semantic domain. The subscript is omitted when context determines the category.

Common semantic functions:

$[[τ]] : Type \to Set$ : the set of values of type $τ$ .
$[[e]]_{ρ} : Expr \to D_{⊥}$ : the meaning of expression $e$ under value environment $ρ$ , where $D_{⊥}$ adjoins a bottom element to handle non-terminating or budget-exceeded computations.
$[[l]] : Lens \to (S \to V) \times (S \times V \times C \to S) \times (S \to C)$ : the meaning of a lens $l$ as a triple of functions.
$[[T]] : Theory \to Cat$ : the category-with-families generated by a GAT presentation.

The bottom element

In the expression language, evaluation is total within a step budget but the budget can be exceeded. We model this by adjoining a bottom element $⊥$ to the value domain: $D_{⊥} = D \cup {⊥}$ . Reaching $⊥$ corresponds to ExprError::StepLimitExceeded at runtime.

Equality

Equality between values, types, and theories is definitional unless otherwise stated. Equality between schemas is structural up to alpha-renaming of bound names. Equality between morphisms is judgemental: $f = g : A \to B$ when $f$ and $g$ have the same source, the same target, and agree on every input.

panproto