Arities in LF

Arities in LF refer to the number of reducible parameters that a given term can take The syntax of arities is quite minimal, a term is eiter fully reduced, 0, or it takes a reducible parameter, A ->> B

Simplification of Types

The arities are first defined by their relationship to types, specifically through a erasure relationship.

1. If s is a atomic sort, then |s| = 0
2. |{x A} B| = |A| ->> |B| (the arguement is irrelevant, we’ll get to that)
3. |F x| = |F|

Because terms only every appear as arguements in types, we can safely ignore the context