Symbol Reference: Expression — Syntactic AST Expression Sort Constructor (.Expression)

Personal Symbol Reference Page in MKTD1 & MKTD2 (Morse-Kelley + Tarski + Dunaev) — All Personal Symbol Pages → | Full Symbol Registry →

Formula Display:
Proof Trees:

Expression \(\mathsf{Expression}\) — Syntactic AST Expression Sort Constructor (.Expression)

Postfix sort constructor A.Expression mapping any semantic sort A (such as Class, Bool, Ctx) to the syntactic sort of its AST expressions (e.g., Class.Expression, Bool.Expression = Fm).

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
Expression
\(\mathsf{Expression}\)
Category Metatheoretic AST Sorts
SML AST Constructor Kernel AST Symbol / Sort Constructor in typetheory.ML (Class_p / Truth_p / EXP / UCol)
Constructor Arguments Typed arguments as specified by the Signature / Sort field above
Metatype / Signature Sort Constructor (A → A.Expression)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{Expression}
How to Understand It

SML AST Representation: Enforces the off-by-one metalevel invariant between semantic values (A) and checkable syntactic AST expressions (A.Expression).
Canonical Law / Usage (t : X.Expression)
Related Symbols & Kernel Entries