An axiomatization of residuals

We present a simple axiomatization of residual relation in
conflict-free models of computation, such as Peano arithmetic or the
lambda-calculus, originated from work of J.J. Le'vy. When combined
with a general, abstract concept of "result of computation", such as
head-normal forms or Bohm-trees in the lambda-calculus, the
axiomatization allows us to prove the normalization and optimality
results in a very general form. Further, we can define an
event-structure style semantics for conflict-free computation in
general (where redexes can be replicated or erased), and formalize a
concept of "modularity" or "independence" of computation, allowing us
to build Euclid-like Geometry of Reduction Spaces, supporting a
concept of "decomposition" of computation with respect to a
basis. Finally, we show how the axiomatization of residuals can be
translated into partial orders more directly, in the spirit of Kahn &
Plotkin's work on concrete domains, yielding a concept of partial
orders that can capture duplication of redexes during computation.

Joint work with John Glauert, UEA, UK.