### Axioms for recursion in call-by-value

Masahito Hasegawa and Yoshihiko Kakutani
*Higher-Order and Symbolic Computation* **15**(2/3):235-264, September 2002

### Abstract

We propose an axiomatization of fixpoint operators in typed
call-by-value programming languages, and give its justifications in
two ways.
First, it is shown to be sound and complete for the notion of uniform
T-fixpoint operators of Simpson and Plotkin.
Second, the axioms precisely account for Filinski's fixpoint operator
derived from an iterator (infinite loop constructor) in the presence
of first-class continuations, provided that we define the uniformity
principle on such an iterator via a notion of effect-freeness
(centrality).
We then explain how these two results are related in terms of the
underlying categorical structures.

**keywords:** recursion, iteration, call-by-value, continuations,
categorical semantics.

### Pointers to Related Work

- A. Filinski,
**Recursion from iteration**.
*Lisp and Symbolic Comput.* **7**(1) (1994) 11-38.
- Y. Kakutani,
**Duality between call-by-name recursion and call-by-value iteration**.
In *Proc. Computer Science Logic*, Springer LNCS (2002) pp. 506-521.
- P.
Selinger,
**Control categories and duality: on the categorical semantics of
the lambda-mu calculus**.
*Math. Structures Comput. Sci.* **11**(2) (2001) 207-260.
- A.K. Simpson and
G.D. Plotkin,
**Complete axioms for categorical fixed-point operators**.
In *Proc. 15th Annual Symposium on Logic in Computer
Science* (2000) pp.30-41.

Back to Hassei's
Research Page / Home Page