This section may be skipped on the first reading,
as
the informal description of the type system given in section 
should meet the needs of most readers.
This section consists of two parts. First, we give the formal definition of 's type system by means of a recursive definition of the necessary predicates. Then, for ease of understanding and reference, from the definition we extract criteria for typehood and membership. Those who do read this section may benefit by reading the latter part first.