Confluence via strong normalisation in an algebraic calculus with rewriting
43
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
43
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
- linear logic
- origin linear
- algebraic ?-calculus
- algebraic
- universidad nacional de rosario
Publié par
Langue
English
Confluence 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 Jaskelioff
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 Differential -calculus: capturing linearity à la Linear Logic
! Removing the differential 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
Confluence issues
Y = (x:(B + (x)x))x:(B + (x)x)B
Y ! B +Y ! B +B +Y !:::B B B
3/15
