Prof. Martin Hofmann, Büchi Types

Buchi Types

(joint work with Wei Chen)

In previous work we have been using types (or rather type-and-effect systems) to analyse the runtime behaviour of object-oriented programs and in particular the adherence to programming guidelines and resource consumption.

We were now trying to extend this to infinitary behaviour, ie. specification based on w-regular languages and/or Buchi automata so as to be able to capture fairness and liveness properties.

Perhaps surprisingly, the usual typing rule for recursive functions does not work in this case:

Suppose that a() and b() are functions of type unit->unit that issue an a-event, respectively a b-event. Thus, we would get an effect typing like a() : unit & {a} and b() : unit & {b}. Now let S denote the w-regular language (a^*b)^w, i.e. infinitely many b's and suppose that m() is defined recursively by m(){a();m()}. With the usual typing rule for recursion we could then justify the erroneous effect typing m():unit & S, for assuming m():unit & S we derive a();m():aS hence a();m():S since aS=S.

Thus, the recursive typing rule (assume any type for recursive calls justify it for the body) is not sound for infinitary behaviours.

We have worked out the following alternative typing rule: given a recursive definition m(){body}  assume m():unit&X for a "variable" X. Derive body:unit&AX+B for A a language of finite words and B a language of infinite words. Conclude from this that m():unit&A^*B+A^w. This is sound, useful, and even complete in a sense that I will make precise. In the example from m():unit&X we conclude body:unit&aX+0 so that, unconditionally, we get m():unit&a^w.