We present a general semantic universe of call-by-value computation
based on elements of game semantics, and validate its appropriateness
as a semantic universe by the full abstraction result for
call-by-value PCF, a generic typed programming language with
call-by-value evaluation. The key idea is to consider the distinction
between call-by-name and call-by-value as that of the structure of
information flow, which determines the basic form of games. In this
way the call-by-name computation and call-by-value computation arise
as two independent instances of sequential functional computation with
distinct algebraic structures. We elucidate the type structures of the
universe following the standard categorical framework developed in the
context of domain theory. Mutual relationship between the presented
category of games and the corresponding call-by-name universe is also
clarified.
The essential feature of this semantic representation of call-by-value
computation is clean behavioural articulation of the concerned class
of functional computation where categorical type structures and
structures of interaction go hand in hand. The structure of
interaction is representable as a specific form of name passing
interactions, which is in close connection to Milner's encoding of
call-by-value lambda calculus. This aspect will also be discussed,
together with our recent development based on the present work, if the
time allows.
(Nobuko Yoshida, first presented at ICALP'97, Bologna.)
|