Guarded Recursion

A recursive definition is guarded whenever there provably is some productive work done before a recursive call takes place.

The notion of guardedness is ubiquituous throughout the literature on process calculi. It also appears as a technique in the semantics of programming languages, through the techniques of step-indexing and guarded domain theory.

In \lambda-calculus and type theory

The need to have guarded recursion in \lambda-calculi and type theories arises from the need to have a safe way to handle infinite objects.

See the main article.

Contractiveness

One of the mathematical interpretations of guardedness is through contractive maps in ultrametric spaces.

Please expand.

References

Please expand.