Archive for November, 2012

Closures and fixpoints

Introduction Recursive definitions of functions (and processes as we well see later) are fixpoint equations. The simple example of the recursive definiton of the factorial function can be used to illustrate this fact. fact(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*fact(n-1) end end This definition is equivalent to the following assertion. fact_all: […]

, ,

Leave a comment

Functions and Complete Partial Orders

Motivation Why study complete partial orders? Let us look at some simple examples. Everybody knows the recursive definition of the factorial function. In our programming language the definition looks like: factorial(n:NATURAL): NATURAL ensure Result = if n=0 then 1 else n*factorial(n-1) end end But this is not a classical definition. A classical definition of a […]