Martin Hofmann: What is a pure functional?
29.01.2010 14:15
We investigate the following question. Given a higher-order SML function
F : (int->int) -> int
how can we rigorously specify that F is pure, ie produces no side-effects
other than those arising from calling its functional argument.
(If you don't like higher-order SML functions think of F as a method that
may invoke a library function. It should produce no side-effects other
than those that might arise from calls to the library function.)
We show that existing methods based on preservation of invariants and
relational parametricity are insufficient for this purpose and thus define
a new notion that captures purity in the sense that for any functional F
that is pure in this sense there exists a corresponding question-answer
strategy, ie an element of the datatype
type tree = Answer of int | Question of int * (int -> tree)
This work is motivated by the ongoing effort to verify a new fixpoint
algorithm by Helmut Seidl which takes such a functional as input (or
rather a functional of type ((Variables->Domain)->(Variables->Domain)) and
whose correctness is contingent on this functional to be pure.
Artikelaktionen
abgelegt unter:
Oberseminar