p?(x: T) : INDUCTIVE bool
  = tau(p?)(x)

where

• tau: [[T -> bool] -> [T -> bool]]

and, more precisely:

• tau: (monotonic?[T])
• which means that if A≤B, then tau(A) ≤ tau(B), where ≤ stands for subset inclusion (see subset? predicate definition in PVS prelude).

The meaning of the the above inductive definition is simply

p?: [T -> bool]
  = mu(tau)

where

• mu(tau) designates the least fixed point of tau functional (a functional is a function of a function): this least fixed point exists and is unique in this context;
• by definition, a fixed point of tau is a set Q: [T -> bool] such that tau(Q) = Q.

Remarks:

• There is no termination condition for an inductive definition: termination is replaced with monotonicity; inductive definitions are mathematical, not computational;
• The monotonicity of tau underlying functional, in an inductive definition, is often automatically proved by PVS;
• Although mu does not yield a least fixpoint when tau is not monotonic, mu(tau) is still defined in PVS prelude as the intersection of all fixed points of tau, which is defined even if tau has no fixed point, since we are in typed set theory: in this case, mu(tau) = fullset[T] (see PVS prelude);
• Inductive definitions may take more than one parameter x: recall that a function of N parameters may be identified with a function of one parameters, so that the above presentation is appropriate.

General fixed point theory

General fixed point theory considers a complete partial order structure [E, ≤], that is:

• E is partially ordered by ≤, meaning that ≤ is a reflexive, transitive and antisymmetric relation in E;
• E has a bottom (least) element, often denoted ;
• Every chain c in E has a least upper bound (lub) in E, where:
• a chain c in E is a totally ordered subset of E.
• Remark: Most textbooks assume c to be non empty; this is unnecessary, because the empty set admits E bottom element for lub.

In this general context, one of the main theorems is:

Every monotonic functional tau: [E -> E] admits a least fixed point, denoted mu(tau), where “tau monotonic“ means:

x ≤ y   =>  tau(x) ≤ tau(y), for all x, y in E.

A simple consequence of this theorem is fixed point induction:

   tau(p) ≤ p 
----------------
  mu(tau) ≤ p

Fixed point induction in PVS

In the context of PVS inductive sets:

• E correspond to a type of the form [T -> bool], whose elements are all sets of elements of type T;
• The partial order ≤ is set inclusion, denoted subset? or more precisely subset?[T] in sets PVS prelude theory, and ≤ in mucalculus PVS prelude theory;
• The bottom element  is emptyset[T];
• The existence of a lub for a chain of sets, or actually any set of sets, is trivially satisfied, since every set of sets admits its union for lub;
• Fixed point induction is useful for proving that all elements in mu(tau) satisfy some property p, in other words, that mu(tau) is a subset of p:
  (FORALL (x: T):  tau(p)(x)  IMPLIES  p(x)) 
  ------------------------------------------- 
  (FORALL (x: T):  mu(tau)(x)  IMPLIES  p(x))

• PVS actually generates as an axiom a specialized version of the above, for each INDUCTIVE definition of a set.

Beware that the INDUCT proof command only deals with well founded induction: it has not been extended to fixed point induction, although this could be done; hence, the user has to explicitely use axioms generated by PVS. The name of the (most useful) axiom is derived from the name of the inductive predicate, by adding weak_induction suffix: