202307242307

Type :Note Tags : Type Theory

---

Atomic Types

A term of an atomic type is reducible iff it is strongly normalizable so every term must satisfy the following conditions

• CR1 is a Tautology
• CR2 If $t$ is strongly normalizable then every term $t^{\prime }$ which reduces $t$ to is also strongly normalizable.
• CR3 A reduction path leaving $t$ must be through one of the $t^{\prime }$, which are all strongly normalizable, and so if finite, and $v(t)$ is maximum of $v(t^{\prime })+1$ where $t^{\prime }$ vary over one step conversions from $t$

---

References

Product Type Arrow Type