Axioms for recursion in call-by-value
Masahito Hasegawa and Yoshihiko Kakutani
Higher-Order and Symbolic Computation 15(2/3):235-264, September 2002
We propose an axiomatization of fixpoint operators in typed
call-by-value programming languages, and give its justifications in
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
We then explain how these two results are related in terms of the
underlying categorical structures.
keywords: recursion, iteration, call-by-value, continuations,
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.
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
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