Confluence via strong normalisation in an algebraic calculus with rewriting
43 Pages
English
Gain access to the library to view online
Learn more

Confluence via strong normalisation in an algebraic calculus with rewriting

-

Gain access to the library to view online
Learn more
43 Pages
English

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


Subjects

Informations

Published by
Reads 14
Language English

Exrait

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