Stratagem home page
Stratagem is a research prototype system illustrating some recent
theoretical ideas in game semantics, written in Standard ML of New Jersey.
However, you don't have to be an expert in game semantics to use it -
in fact, Stratagem is largely intended
to illustrate some of the curious programming tricks that
these theoretical ideas make possible.
It also serves as a fun and relatively painless way of absorbing some of
the main ideas of game semantics, if you're interested.
Exactly what it does is hard to explain in a few words,
but quite easy to grasp once you see it in action.
The key idea is that given some operation or function supplied by the user,
Stratagem extracts the underlying "computation strategy" and allows it to
be explored and manipulated in various ways.
Possible applications include
execution tracing, interactive execution, and program optimization.
The system makes essential use of explicit continuations, and
currently only runs on the New Jersey SML compiler. I have tested it on
version 110.0.7 - please let me know if you have problems running
it on other versions. (The current version (1.1) fixes a problem in
version 1.0 which meant that it didn't compile under NJ-SML 110.42.
Many thanks to Ethan Aubin for his help with this.)
To use Stratagem, just download the
source code and
the user documentation
which serves as a walkthrough introduction to the system's capabilities.
Then follow the steps described in the latter.
The Stratagem system could potentially be of interest to workers in
the following areas:
- Game semantics. The system provides a "workbench" for one version
of game semantics, offers a convenient way of exploring the game
strategy for ML programs, and may be useful as a teaching tool.
- Program logics and verification. Stratagem offers a relatively
programmer-friendly way of understanding some ideas from semantics
that are likely to have applications to program logics in the near
future.
- Continuations. The system may be of interest as a non-trivial
example of a program making essential use of continuations.
It also seems to offer a helpful way of understanding much of what
continuations do, without the need for explicit continuation types.
- Execution tracing and debugging tools. Stratagem provides a kind
of execution tracing facility for ML programs, with some unusual
capabilities (e.g. interactive exploration of alternative execution
paths) which may be useful for debugging ML programs. Another
unusual feature is that the execution tracer runs within the same
ML session as the user's program - perhaps there is some interesting
way of exploiting this fact?
- Program optimization. Stratagem supplies a "generic optimizer" for
computation strategies. In some cases, this can lead to a genuine
speed-up for the user's already compiled program.
- Lazy and higher order programming. For programs involving lazy data
structures and higher order functions, it can often be difficult to
understand their run-time behaviour operationally - "what happens
when". The execution tracing facilities of Stratagem may be useful
for understanding such programs better.
- Teaching ML. For newcomers to ML, Stratagem might be useful as a
teaching tool - for example, for viewing the recursion unfoldings of
a recursively defined function.
The current version (1.1) is intended as a concept demonstrator rather than
a serious debugging tool - the full range of ML datatypes is not yet
supported - but it suffices to illustrate all the basic ideas and allows
the user to perform some complex and interesting experiments.
John Longley
Last modified: Mon Jun 5 13:31:21 BST 2006