A simple functional programming language

• Basic type: nat (meaning natural numbers)
• Types:
  • nat is a type
  • If A and B are both types, then A -> B is also a type
  • ->, if parentheses are omitted, associates to the right: nat -> nat -> nat means nat -> (nat -> nat).
• Constants:
  • natural numbers in decimal notation;
  • +; *
• Variables: xi (i is a natural number in decimal notation)
• Context: a sequence of lines of the form xi : A, where xi is a type and A is a type.
• Terms: (each term has a unique type!)
  • every variable xi is a term, and its type is the corresponding A from the context;
  • every natural constant is a term of type nat;
  • + and * are terms of type nat -> nat -> nat;
  • if u is a term of type A -> B and v is a term of type A, then uv is a term of type B (if u and v have types not of the specified form, uv is not a correct term!);
  • if w is a term of type B and xi is a variable of type A (as declared in the context), then lambda xi . w is a term of type A -> B.
    For simplicity, we always suppose that the variable xi is never used further outside this subterm bounded by lambda.
  • Precedence: lambda is stronger than application (uv); application associates to the left (uvw means (uv)w).
• β-reduction: replace any subterm of the form (lambda xi . u)v with u[xi := v], i.e., u with any occurrence of xi replaced with v.
• A functional program of the simple functional language consists of:
  • a context (see above);
  • a term.
• The interpreter should:
  1. check that the term is correct (including type checking);
  2. perform β-reductions until it becomes impossible (i.e., the term is in the normal form; Strong Normalization and Church-Rosser properties guarantee that the normal form exists and does not depend on the order of reduction steps);
  3. if the resulting normal form is of type nat and doesn't include variables, compute it as a natural number.