Confluence via strong normalisation in an algebraic calculus with rewriting

pages

English

Documents

Écrit par
Pablo Buiras1

Publié par
profil-urra-2012

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

profil-urra-2012

Nombre de lectures

Langue

English

Confluence via strong normalisation in an algebraic ?-calculus with rewriting – Accepted in LSFA 2011. To appear in EPTCS – Pablo Buiras1 Alejandro Díaz-Caro2 Mauro Jaskelioff1,3 1Universidad Nacional de Rosario, FCEIA, Argentina 2Université de Grenoble, LIG, France 3CIFASIS-CONICET, Argentina Recontre QuAND • July 18, 2011 • Marseille, France

linear logic

origin linear

algebraic ?-calculus

algebraic

universidad nacional de rosario

Voir

Publié par

profil-urra-2012

Nombre de lectures

Langue

English

Conﬂuence via strong normalisation in an
algebraic -calculus with rewriting
– Accepted in LSFA 2011. To appear in EPTCS –
1 2 1;3Pablo Buiras Alejandro Díaz-Caro Mauro Jaskelioﬀ
1Universidad Nacional de Rosario, FCEIA, Argentina
2Université de Grenoble, LIG, France
3CIFASIS-CONICET, Argentina
Recontre QuAND July 18, 2011 Marseille, FranceM;N ::= xj x:Mj (M)Nj M +Nj :Mj 0
Beta reduction:
(x:M)N! M[x := N]
“Algebraic” reductions:
:M +:M! ( +):M;
(M)(N +N )! (M)N + (M)N ;1 2 1 2...
...
...
(oriented version of the axioms of vectorial spaces)
Two origins:
I Diﬀerential -calculus: capturing linearity à la Linear Logic
! Removing the diﬀerential operator: Algebraic -calculus ( ) [Vaux’09]alg
I Quantum computing: superposition of programs
! Linearity as in algebra: Linear-algebraic -calculus ( )lin
[Arrighi,Dowek’08]
2/15M;N ::= xj x:Mj (M)Nj M +Nj :Mj 0
Beta reduction:
(x:M)N! M[x := N]
“Algebraic” reductions:
:M +:M! ( +):M;
(M)(N +N )! (M)N + (M)N ;1 2 1 2...
...
...
(oriented version of the axioms of vectorial spaces)
alg lin
Origin Linear Logic Quantum computing
Strategy Call-by-name Call-by-value
2/15Y +Y ! B +Y +Y ! B +2:YB B B B B
#
2:Y ... and equalitiesB
Solution 2 ( ):alg
Solution 3:Only positive numbers
forbid1! (type system)
Y + ( 1):Y ! (1 1):Y ! 0B B B
#
Solution 1 ( ):linB +Y + ( 1):YB B
:M +:M! ( +):M
#
only if M is closed-normal
B
and others similar restrictions
Objective: to forbid11
Conﬂuence issues
Y = (x:(B + (x)x))x:(B + (x)x)B
Y ! B +Y ! B +B +Y !:::B B B
3/15