Confluence via strong normalisation in an algebraic calculus with rewriting

Pablo Buiras1

Description

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

Sujets

• Université de Grenoble
• Linear logic
• Algebraic
• Universidad Nacional de Rosario

Informations

• Publié par: profil-urra-2012
• Nombre de lectures: 14
• Langue: English

Extrait

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