Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces
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 vec...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Alexandru Ioan Cuza University of Iasi
2014-12-01
|
| Series: | Scientific Annals of Computer Science |
| Online Access: | http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_5.pdf |
| id |
doaj-3f60d8252dc4439a968d1741c2f072ab |
|---|---|
| record_format |
Article |
| spelling |
doaj-3f60d8252dc4439a968d1741c2f072ab2020-11-25T02:44:07ZengAlexandru Ioan Cuza University of IasiScientific Annals of Computer Science1843-81212248-26952014-12-01XXIV232536810.7561/SACS.2014.2.325Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector SpacesB. ValironS. ZdancewicIn 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.http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_5.pdf |
| collection |
DOAJ |
| language |
English |
| format |
Article |
| sources |
DOAJ |
| author |
B. Valiron S. Zdancewic |
| spellingShingle |
B. Valiron S. Zdancewic Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces Scientific Annals of Computer Science |
| author_facet |
B. Valiron S. Zdancewic |
| author_sort |
B. Valiron |
| title |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces |
| title_short |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces |
| title_full |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces |
| title_fullStr |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces |
| title_full_unstemmed |
Modeling Simply-Typed Lambda Calculi in the Category of Finite Vector Spaces |
| title_sort |
modeling simply-typed lambda calculi in the category of finite vector spaces |
| publisher |
Alexandru Ioan Cuza University of Iasi |
| series |
Scientific Annals of Computer Science |
| issn |
1843-8121 2248-2695 |
| publishDate |
2014-12-01 |
| description |
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. |
| url |
http://www.info.uaic.ro/bin/download/Annals/XXIV2/XXIV2_5.pdf |
| work_keys_str_mv |
AT bvaliron modelingsimplytypedlambdacalculiinthecategoryoffinitevectorspaces AT szdancewic modelingsimplytypedlambdacalculiinthecategoryoffinitevectorspaces |
| _version_ |
1724767371973885952 |