§ Logical Predicates (OPLSS '12)

• $R_\tau(e)$ has three conditions:
• (1) $e$ has type $\tau$
• (2) $e$ has the property of interest ( $e$ strongly normalizes / has normal form)
• (3) The set $R\tau$ is closed under eliminators!
• My intuition for (3) is that expressions are "freely built" under constructors. On the other hand, it is eliminators that perform computation, so we need $R_\tau$ to be closed under "computation" or "elimination"
• Video