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
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 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:
A simple consequence of this theorem is fixed point induction:
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.
Bruno Dutertre library
is a PVS implementation of fixed point theory specialized to sets. The theory also elegantly introduces the greatest fixed point of a monotonic functional, nu, as mu's dual, using set complement. This theory clearly shows that the INDUCTIVE PVS feature is not essential: inductive sets may be equivalently defined with more primitive PVS concepts, simply using mu function. However, this feature is nevertheless convenient in practice. |