Martin Hofmann: What is a pure functional?
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.
abgelegt unter: Oberseminar