Symbol Reference: eval / Eval_(A,ρ) — Composite Code Evaluation Operator (Eval_(A,ρ)(c) = Val_ρ(μ_A(Dec_A(c))))

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

Formula Display:
Proof Trees:

eval / Eval_(A,ρ) \(\mathsf{eval} \; / \; \mathsf{Eval}_{(A,\rho)}\) — Composite Code Evaluation Operator (Eval_(A,ρ)(c) = Val_ρ(μ_A(Dec_A(c))))

Composes syntactic decoding Dec_A : Class → A.Expression, type-indexed expression translation μ_A : A.Expression → Class.Expression, and semantic valuation Val_ρ : Class.Expression → Class.

Field Mathematical & Kernel Specification (MKTD1 / MKTD2)
Symbol
eval / Eval_(A,ρ)
\(\mathsf{eval} \; / \; \mathsf{Eval}_{(A,\rho)}\)
Category Embedding & Interpretation
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 Class → Class (or Class → Bool for Fm codes)
Binder Status See Category & Signature above
Defining Kernel Entries (ML Labels) See Related Symbols & Kernel Entries below.
LaTeX Form \mathsf{eval} \; / \; \mathsf{Eval}_{(A,\rho)}
How to Understand It

How to Understand eval / Eval_(A,ρ):

With the type-indexed translation μ_A and assignment-indexed valuation Val_ρ kept explicitly distinct, the semantic evaluation of a class code c ∈ Code_A ⊆ V is the three-stage composite:

Eval_(A,ρ)(c) = Val_ρ(μ_A(Dec_A(c))) = μ^val_ρ(Dec_A(c))

  • Well-Typed Round-Trip on Coded Expressions: For any syntactic expression e : A.Expression, Eval_(A,ρ)(Enc_A(e)) = Val_ρ(μ_A(e)) = μ^val_ρ(e) because Dec_A(Enc_A(e)) = e.
  • Stratification via Tarski Universes: By Tarski's Undefinability of Truth, a single unstratified truth/evaluation predicate for all formulas over the entire universe cannot be internal to the same level; in MKTD1 / MKTD2, Tarski's Axiom of Universes (Entry AxmTarskiUniverses (3.70)) provides set-sized universes supporting internal model valuations.
Canonical Law / Usage Eval_(A,ρ)(Enc_A(e)) = Val_ρ(μ_A(e))
Related Symbols & Kernel Entries