## § 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