previous up next
Go backward to Lifted Domains
Go up to Top
RISC-Linz logo

Recursive Function Definitions

Recursive function definitions need not define a function uniquely!

q(x) = (equals x zero) -> one
[] q(plus x one)
f1(x)={
one if x = zero
_|_ otherwise
f2(x)={
one if x = zero
two otherwise
f3(x) = one

How to formmalize that q yields the intended denotation f1?

(the problem will be handled later)

(same with recursive domain definitions)


Author: Wolfgang Schreiner
Last Modification: October 14, 1997

previous up next