A Semantics for Functions and Behaviours

The functional animation language Fran allows animations to be programmed in a novel way. Fran provides an abstract datatype of ``behaviours'' that represent time varying values such as the position of moving objects, together with a simple set of operators for constructing behaviours. More generally, this approach has potential for other kinds of real-time systems that consist of interactive components that evolve over time. We introduce a small functional language, CONTROL, which has behaviours and operators that are similar to those in Fran. Our language improves on Fran in certain key areas, in particular, by eliminating start times and distinguishing between recursive functions and recursive behaviours. Our main contribution is to provide a complete formal semantics for CONTROL, which Fran lacks. This semantics provides a precise description of the language and can be used as the basis for proving that programs are correct. The semantics is defined under the assumption that real number computations and operations on behaviours are exact. Behaviours are modelled as functions of continuous time, and this approach is combined with the standard approach to the semantics of functional languages. This combination requires some novel techniques, particularly for handling recursively defined behaviours.