Abstract
Finiteness spaces constitute a categorical model of Linear Logic (LL) whose objects can be seen as linearly topologised spaces, (a class of topological vector spaces introduced by Lefschetz in 1942) and morphisms as continuous linear maps. First, we recall definitions of finiteness spaces and describe their basic properties deduced from the general theory of linearly topologised spaces. Then we give an interpretation of LL based on linear algebra. Second, thanks to separation properties, we can introduce an algebraic notion of totality candidate in the framework of linearly topologised spaces: a totality candidate is a closed affine subspace which does not contain 0. We show that finiteness spaces with totality candidates constitute a model of classical LL. Finally, we give a barycentric simply typed lambda-calculus, with booleans \({\mathcal{B}}\) and a conditional operator, which can be interpreted in this model. We prove completeness at type \({\mathcal{B}}^n\to{\mathcal{B}}\) for every n by an algebraic method.
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
Blute, R.F., Scott, P.J.: Linear Lauchli semantics. Annals of Pure and Applied Logic (1996)
Chu, P.H.: Autonomous categories, chapter Constructing*-autonomous categories. Lecture Notes in Mathematics 11 (1979)
Colson, L., Ehrhard, T.: On strong stability and higher-order sequentiality. In: Proceedings of Symposium on Logic in Computer Science, 1994. LICS 1994, pp. 103–108 (1994)
Ehrhard, T.: On finiteness spaces and extensional presheaves over the Lawvere theory of polynomials. Journal of Pure and Applied Algebra (to appear)
Ehrhard, T.: Hypercoherences: A strongly stable model of linear logic. Mathematical Structures in Computer Science 3(4), 365–385 (1993)
Ehrhard, T.: Finiteness spaces. Mathematical Structures in Comp. Sci. 15(4) (2005)
Fischer, H.R., Gross, H.: Tensorprodukte linearer topologien. Math. Annalen 160 (1965)
Girard, J.-Y.: The system F of variable types, fifteen years later. Theoretical Computer Science 45, 159–192 (1986)
Girard, J.Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
Girard, J.Y.: Le point aveugle cours de logique Tome 1 Vers la perfection Visions des sciences. Hermann (2006)
Grothendieck, A.: Produits tensoriels topologiques et espaces nuclaires, vol. 16. American Mathematical Society (1955)
Hyland, M., Schalk, A.: Glueing and orthogonality for models of linear logic. Theoretical Computer Science 294(1-2), 183–231 (2003)
Köthe, G.: Topological Vector Spaces I. Springer, Heidelberg (1979)
Lafont, Y., Streicher, T.: Games semantics for linear logic. In: Proceedings of Sixth Annual IEEE Symposium on Logic in Computer Science, 1991. LICS 1991, pp. 43–50 (1991)
Lefschetz, S., et al.: Algebraic topology. American Mathematical Society (1942)
Loader, R.: Linear logic, totality and full completeness. In: Proceedings of Symposium on Logic in Computer Science, 1994. LICS 1994, pp. 292–298 (1994)
Vaux, L.: On linear combinations of λ-terms. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 374–388. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tasson, C. (2009). Algebraic Totality, towards Completeness. In: Curien, PL. (eds) Typed Lambda Calculi and Applications. TLCA 2009. Lecture Notes in Computer Science, vol 5608. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02273-9_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-02273-9_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02272-2
Online ISBN: 978-3-642-02273-9
eBook Packages: Computer ScienceComputer Science (R0)