Localisation

Adresses

Aix-Marseille Université
Institut de Mathématiques de Marseille (I2M) - UMR 7373
Site Saint-Charles : 3 place Victor Hugo, Case 19, 13331 Marseille Cedex 3
Site Luminy : Campus de Luminy - Case 907 - 13288 Marseille Cedex 9

Séminaire

Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi

Benoît Valiron
PPS, Université Paris-Diderot
https://www.monoidal.net/

Date(s) : 28/03/2014   iCal
14h00 - 15h00

In this paper we use finite vector spaces (finite dimension, over finite fields) as a non-standard computational model 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. The second model is not complete, but we develop an algebraic extension of the finite lambda calculus that recovers completeness. The relationship between the two semantics is described, and several examples based on Church numerals are presented.

Catégories


Secured By miniOrange