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.
The need to have guarded recursion in -calculi and type theories arises from the need to have a safe way to handle infinite objects.
See the main article.
One of the mathematical interpretations of guardedness is through contractive maps in ultrametric spaces.
Please expand.
Please expand.