Axioms for recursion in call-by-value (extended abstract)
Masahito Hasegawa and Yoshihiko Kakutani
In
Proc.
Foundations of Software Science and Computation Structures
(FoSSaCS 2001),
Springer LNCS
2030 (2001) 246-260
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 controls, provided that we define the uniformity
principle on such an iterator via a notion of effect-freeness
(centrality).
We also investigate how these two results are related in terms of the
underlying categorical models.
© Springer-Verlag 2001
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