Lambda the Ultimate

Endofunctions are functions f of type A->A where A can be any type. Since all functions are potentially partial functions we can use endofunctions to model linked structures.

E.g. if we have an object which has an optional reference to an object of the same type, the optional reference can be viewed as a partial function f of type A->A. If the reference to the next object is void (there is no next object because we are at the end of a linked list or we have reached the root of a tree following the parent links) then the corresponding function f is undefined for this specific object.

The paper "Endofunctions, cycles and chains" describes endofunctions and derives assertions about endofunctions which are important to reason about linked structures. It is based on the papers "Complete lattices and closure systems" and "Closures and fixpoints".