Abstract
In existing game models, total functionals have no simple characterization neither in term of game strategies, nor in term of the total set-theoretical functionals they define. We show that the situation changes if we extend the usual notion of game by allowing infinite plays. Total functionals are, now, exactly those having a tree-strategy in which all branches end in a last move, winning for the strategy. Total functionals now define (via an extensional collapse) all set-theoretical functionals. Our model is concrete: we used infinite computations only to have a nice characterization of totality. A computation may be infinite only when the input is a discontinous functional; in practice, never.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky, “Semantics of Interaction”, in Semantics and Logics of Computation, A. Pitts and p. Dybjer eds., Cambridge University Press 1997, 1–31.
S. Abramsky, R. Jagadeesan, “Games and full completeness for multiplicative linear logic”, Journal of Symbolic Logic 59(2), 1994, 543–574.
S. Abramsky, R. Jagadeesan, P. Malacaria, “Full abstraction for PCF”, Proceedings of TACS’94, Springer Lecture Notes in Computer Science 789, 1994, 1–15.
S. Berardi, M. Bezem, T. Coquand, “On the Constructive Content of the Axiom of Choice”, Journal of Symbolic Logic, to appear.
S. Berardi, T. Coquand, “Transfinite Games”, September 1996.
A. Blass, “A game semantics for linear logic”, Annals of Pure and Applied Logic 56, 183–220.
T. Coquand, “A Semantics of Evidence for Classical Arithmetic”, Journal of Symbolic Logic 60, 1995, 325–337.
H. Herbelin. Séequents qu’on calcule. Ph.D. thesis, Univeristy of Paris VII, 1995.
J.M.E. Hyland, “Game Semantics”, in Semantics and Logics of Computation, A. Pitts and p. Dybjer eds., Cambridge University Press 1997, 131–184.
J.M.E. Hyland, C.-H.L. Ong, “On full abstraction for PCF”, available by ftp at ftp://ftp.comlab.ox.ac.uk/pub/Documents/techpapers/Luke.Ong/ as pcf.ps.gz, 1994.
H. Nickau, Hereditarily Sequential Functionals: A Game-Theoretic Approach to Sequentiality, Shaker Verlag, Achen 1996.
G. Plotkin, “Full Abstraction, Totality and PCF”, available by ftp at ftp://ftp.lfcs.ed.ac.uk/pub/gdp/ as Totality.ps.gz, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berardi, S., de’Liguoro, U. (1999). Total Functionals and Well-Founded Strategies. In: Girard, JY. (eds) Typed Lambda Calculi and Applications. TLCA 1999. Lecture Notes in Computer Science, vol 1581. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48959-2_6
Download citation
DOI: https://doi.org/10.1007/3-540-48959-2_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65763-7
Online ISBN: 978-3-540-48959-7
eBook Packages: Springer Book Archive