$𝛽$ -computation

A $𝛽$ -computation rule is a conversion rule, usually a judgemental equality, specifying how a connective should compute. Specifically, $𝛽$ -computation specifies the result of an eliminator applied to an introduction. For example, in the untyped λ-calculus, we have

(𝜆 𝑥 . 𝑡) 𝑢 ⇝ 𝛽 𝑡 [𝑢 / 𝑥] .

Internalizing judgemental structure

In terms of Internalizing judgemental structure, if a connective $Υ$ is specified by a family of bijections

𝜄 : 𝐴 Γ ≅ 𝐵 Γ

natural in $Γ$ where

$𝐴 Γ$ is either $T m (Γ, Υ)$ or $T m (Γ . Υ, 𝐴)$ ;
$𝐵 Γ$ is a meta-set constructed from sets of terms (“judgementally-determined structure”)

then $𝛽$ -computation comes from the identity

𝜄 \circ 𝜄 - 1 = i d 𝐵 Γ .

#state/tidy | #lang/en | #SemBr

𝛽-computation

Internalizing judgemental structure

$𝛽$ -computation