History of functions.

Definition set of ordered pairs such that the first elements occurs at most once.

$$ \set{(x,y)} $$

Multiple return values are natural, see the division algorithm. Nearly all programming language support multiple input value, some also multiple return values. Both are not strictly more expressive. Multiple return values can be implemented using tuples. Multiple inputs using currying.

Lambda calculus


Tree based syntax for proof system:

Graphs as more fundamental

Coq's extensible syntax

Remco Bloemen
Math & Engineering