Go backward to q Function Go up to Top Go forward to Factorial Function

Recursive Specifications

The meaning of a recursive specification f=F(f) is taken to be fix(F), the least fixed point of the functional denoted by F.

graph(fix F) = union_i=0^oo graph(Fⁱ(_|_))

• The domain D of F must be a pointed cpo
  • partial ordering on D,
  • every chain in D has a least upper bound in D,
  • D has a least element.
• F must be continuous

  Preserves limits of chains.

• Semantic domains are cpos and their operations are continuous.

  Pointed cpos are created from primitive domains and union domains by lifting.