Dynamic Evaluation
Steve Lack – 26 February 1997
This talk was based on the the articles Sketches and Computation I & II by Dominique Duval and Jean-Claude Reynaud, in Mathematical Structures in Computer Science, 1994. It was given in response to Richard Buckland's comments the previous week about ``angelic non-determinism''.
Duval and Reynaud introduce notions of graph, category, functor, sketch, distributive category, and so on appropriate for the world of locally bidiscrete bicategories. Their sketches have are not necessarily projective, but all designated cones and cocones are required to be finite and discrete (i.e. they amount to product and coproduct specifications in the models.)
They define the terms and expressions of a sketch; the expressions are to be thought of as programs over the sketch, and the terms as possible values of programs. The terms of a projective sketch are shown to constitute an initial model of the sketch. More generally, a (not neccesarily projective) sketch for which the terms constitute an inital model is said to be quasi-projective . In this case every expression is equivalent to some term. Static evaluation is a process of finding a term equivalent to a given expression.
For sketches which are not quasi-projective, one is forced to use dynamic evaluation: given an expression one begins to evaluate it, and as soon as a branch occurs in the program which cannot be resolved, one splits the sketch, by making two (or more) enrichments of the sketch, and then evaluating simultaneously in the various sketches.
Back