Hanno Nickau:
Hereditarily Sequential Functionals
In: Proc. Symp. Logical Foundations of Computer Science: Logic
at St. Petersburg,
Eds. A. Nerode and Yu. V. Matiyasevich,
volume 813 of Lecture Notes in Computer Science, pages 253-264,
Springer-Verlag, 1994.
BibTeX Entry
Compressed Postscript File
Abstract
In order to define models of simply typed functional
programming languages being closer to the operational semantics of
these languages, the notions of sequentiality, stability and seriality
were introduced. These works originated from the definability problem for
PCF, posed in (Scott 1972), and the full abstraction problem for PCF,
raised in (Plotkin 1977).
The presented computation model, forming the class of hereditarily
sequential functionals, is based on a game in which each play
describes the interaction between a functional and its arguments during
a computation. This approach is influenced by the work of Kleene
(1978), Gandy (1967), Kahn and Plotkin
(1978), Berry and Curien
(Berry and Curien 1982, Curien 1986, 1992}, and Cartwright and Felleisen
(1992).
We characterize the computable elements in this model in two
different ways: (a) by recursiveness requirements for the game, and (b) as
definability with the schemata (S1)-(S8), (S11), which is related to
definability in PCF. It turns out that both definitions give the same
class of computable functionals. So a robust notion of (sequential)
computability on higher types is presented.
|
