Published in Volume XXIV, Issue 2, 2014, pages 325-368, doi: 10.7561/SACS.2014.2.325

Authors: B. Valiron, S. Zdancewic

Abstract

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model of linear logic. We first define a simple, finite PCF-like lambda-calculus with booleans, and then we discuss two finite models, one based on finite sets and the other on finite vector spaces. The first model is shown to be fully complete with respect to the operational semantics of the language, while the second model is not. We then develop an algebraic extension of the finite lambda calculus and study two operational semantics: a call-by-name and a call-by-value. These operational semantics are matched with their corresponding natural denotational semantics based on finite vector spaces. The relationship between the various semantics is analyzed, and several examples based on Church numerals are presented.

Full Text (PDF)

References

[1] S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, Vol. 163, pp. 409–470, 2000. http://dx.doi.org/10.1006/inco.2000.2930 .

[2] P. Arrighi, A. Díaz-Caro, and B. Valiron. A type system for the vectorial aspects of the linear-algebraic lambda-calculus. In Proceedings of the 7th International Workshop on Developments of Computational Methods (DCM 2011), Electronic Proceedings in Theoretical Computer Science, Vol. 88, pp. 1–15, 2012. http://dx.doi.org/10.4204/EPTCS.88.1 .

[3] P. Arrighi and A. Díaz Caro. A System F accounting for scalars. Logic Methods in Computer Science, Vol. 8, Paper 11, 2012. http://dx.doi.org/10.2168/LMCS-8(1:11)2012 .

[4] P. Arrighi and G. Dowek. Linear-algebraic λ-calculus: higher-order, encodings, and confluence. In Proceedings of the 19th international conference on Rewriting Techniques and Applications (RTA ’08), Lec- ture Notes in Computer Science, Vol. 5117, pp. 17–31, 2008. http://dx.doi.org/10.1007/978-3-540-70590-1_2 .

[5] N. Benton. A mixed linear and non-linear logic: Proofs, terms and models. In Proceedings of the 8th Workshop on Computer Science Logic, Lecture Notes in Computer Science, Vol. 933, pp 121–135, 1995. http://dx.doi.org/10.1007/BFb0022251 .

[6] G. Bierman. On Intuitionistic Linear Logic. PhD thesis, Cambridge Univ., 1994. Also Tech. Report UCAM-CL-TR-346.

[7] A. Bucciarelli, T. Ehrhard, and G. Manzonetto. A relational semantics for parallelism and non-determinism in a functional setting. Ann. Annals of Pure and Applied Logic, Vol. 163, pp. 918–934, 2012. http://dx.doi.org/10.1016/j.apal.2011.09.008 .

[8] P. de Groote. Strong normalization in a non-deterministic typed lambda-calculus. In Proceedings of the Third International Symposium on Logical Foundations of Computer Science, Lecture Notes in Computer Science, Vol. 813, pp. 142–152, 1994. http://dx.doi.org/10.1007/3-540-58140-5_15 .

[9] A. Díaz-Caro. Du Typage Vectoriel. PhD thesis, Univ. de Grenoble, 2011. Archived online at tel.archives-ouvertes.fr:tel-00631514.

[10] T. Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, Vol. 15, pp. 615–646, 2005. http://dx.doi.org/10.1017/S0960129504004645 .

[11] T. Ehrhard, M. Pagani, and C. Tasson. The computational meaning of probabilistic coherence spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), pp. 87–96, 2011. http://dx.doi.org/10.1109/LICS.2011.29 .

[12] T. Ehrhard and L. Regnier. The differential lambda-calculus. Theoretical Computer Science, Vol. 309, pp. 1–41, 2003. http://dx.doi.org/10.1016/S0304-3975(03)00392-X .

[13] J.-Y. Girard. Linear logic. Theoretical Computer Science, Vol. 50, pp.
1–101, 1987. http://dx.doi.org/10.1016/0304-3975(87)90045-4 .

[14] J.-Y. Girard, A. Scedrov and P. J. Scott. Bounded linear logic: A modular approach to polynomial-time computability. Theoretical Com- puter Science, Vol. 97, pp. 1–65, 1992. http://dx.doi.org/10.1016/0304-3975(92)90386-T .

[15] J.-Y. Girard, Y. Lafont, and P. Taylor. Proof and Types. Cambridge Univ. Press, 1990. Available online at http://www.paultaylor.eu/stable/Proofs%2BTypes.html .

[16] G. G. Hillebrand. Finite Model Theory in the Simply Typed Lambda Calculus. PhD thesis, Brown Univ., 1991. Also Tech. Report CS-94-24.

[17] M. Hyland and A. Schalk. Glueing and orthogonality for models of linear logic. Theoretical Computer Science, Vol. 294, pp. 183–231, 2003. http://dx.doi.org/10.1016/S0304-3975(01)00241-9 .

[18] R. P. James, G. Ortiz, and A. Sabry. Quantum computing over finite fields. Draft, 2011. Found on http://arxiv.org/abs/1101.3764 .

[19] J. Lambek and P. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge Univ. Press, 1994.

[20] S. Lang. Algebra. Springer, 2005.

[21] R. Lidl. Finite fields, Cambridge Univ. Press, 1997.

[22] S. Mac Lane. Categories for the Working Mathematician. Springer, 1998.

[23] R. Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, Vol. 4, pp. 1–22, 1977. http://dx.doi.org/10.1016/0304-3975(77)90053-6 .

[24] G. Plotkin. LCF considered as a programming language. Theoret- ical Computer Science, Vol. 5, pp. 223–255, 1977. http://dx.doi.org/10.1016/0304-3975(77)90044-5 .

[25] V. R. Pratt. Re: Linear logic semantics (barwise). On the TYPES mailing list, February 1992. http://www.seas.upenn.edu/~sweirich/types/archive/1992/msg00047.html .

[26] V. R. Pratt. Chu spaces: Complementarity and uncertainty in rational mechanics. Technical report, Stanford Univ., 1994. Course notes, TEMPUS summer school, 35 pages. http://boole.stanford.edu/pub/bud.pdf .

[27] S. Salvati. Recognizability in the simply typed lambda-calculus. In Pro- ceedings of 16th International Workshop on Logic, Language, Informa- tion and Computation (WoLLIC 2009), Lecture Notes in Computer Sci- ence, Vol. 5514, pp. 48–60, 2009. http://dx.doi.org/10.1007/978-3-642-02261-6_5 .

[28] B. Schumacher and M. D. Westmoreland. Modal quantum theory. In Proceedings of the 7th Workshop on Quantum Physics and Logic, pp. 145–149, 2010. http://www.cs.ox.ac.uk/people/bob.coecke/QPL_proceedings.html .

[29] D. S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY. Theoretical Computer Science, Vol. 121, pp. 411–440, 1993. http://dx.doi.org/10.1016/0304-3975(93)90095-B .

[30] P. Selinger. Order-incompleteness and finite lambda reduction models. Theoretical Computer Science, Vol. 309, pp. 43–63, 2003. http://dx.doi.org/10.1016/S0304-3975(02)00038-5 .

[31] S. Soloviev. Category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, Vol. 22, pp. 1387–1400, 1983. http://dx.doi.org/10.1007/BF01084396 .

[32] B. Valiron. A typed, algebraic, computational lambda-calculus. Math- ematical Structures in Computer Science, Vol. 23, pp. 504–554, 2013. http://dx.doi.org/10.1017/S0960129512000205 .

[33] B. Valiron and S. Zdancewic. Finite vector spaces as model of simply-typed lambda-calculi. In Proceedings of the 11th Interna- tional Colloquium on Theoretical Aspects of Computing (ICTAC 2014), Lecture Notes in Computer Science, Vol. 8687, pp. 442–459, 2014. http://dx.doi.org/10.1007/978-3-319-10882-7_26 .

[34] L. Vaux. The algebraic lambda-calculus. Mathematical Structures in Computer Science, Vol. 19, pp. 1029–1059, 2009. http://dx.doi.org/10.1017/S0960129509990089 .

[35] G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993.

Bibtex

@article{sacscuza:valiron2014mslcitcofvs,
  title={Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces},
  author={B. Valiron and S. Zdancewic},
  journal={Scientific Annals of Computer Science},
  volume={24},
  number={2},
  organization={``A.I. Cuza'' University, Iasi, Romania},
  year={2014},
  pages={325--368},
  doi={10.7561/SACS.2014.2.325},
  publisher={``A.I. Cuza'' University Press}
}