Higher Order Recursion

Algebraic data types can be characterised in many ways.
This paper collects those characterisations.
Further as an application ecoding of games is proposed and
the decision problem of type termination is posed.
Following is the list of data type characterisations :
 - The categorical notion of initial algebra semantics
 - The encoding of data types in System F
 - A combinatorical presentation of the general fold algorithm
 - The relation to context free languages
 - The encoding of algebraic data types in Martin L"of type theory