notesum.ai

Published at November 22

A Rewriting Theory for Quantum Lambda-Calculus

cs.LO

Released Date: November 22, 2024

Authors: Claudia Faggian¹, Gaetan Lopez¹, Benoît Valiron²

Aff.: ¹IRIF, CNRS, Université Paris Cité; ²Université Paris-Saclay, CNRS, CentraleSupélec, ENS Paris-Saclay, Inria

Arxiv: http://arxiv.org/abs/2411.14856v1

Call-by-name $\lambda$ -calculus	Call-by-value $\lambda_{v}$ -calculus	Linear $\lambda_{!}$ -calculus
General reduction: $(\to_{\beta})$	General reduction: $(\to_{\beta_{v}})$	General reduction: $(\to_{\beta_{!}})$
Evaluation: head ( $\to_{h}$ )	Evaluation: weak-left ( $\to_{l}$ )	Evaluation: surface ( $\to_{s}$ )
1. Head factorization:	1. Weak-left factorization:	1. Surface factorization:
$M\to^{}_{\beta}N$ iff $M\to^{}_{h}\cdot\to^{*}_{\neg h}N$	$M\to^{}_{\beta_{v}}N$ iff $M\to^{}_{l}\cdot\to^{*}_{\neg l}N$	$M\to^{}_{\beta_{!}}N$ iff $M\to^{}_{s}\cdot\to^{*}_{\neg s}N$
2. Head normalization:	2. Convergence to a value:	2. Surface factorization:
$M\to^{}_{\beta}H$ iff $M\to^{}_{h}H^{\prime}$	$M\to^{}_{\beta_{v}}V$ iff $M\to^{}_{l}V^{\prime}$	$M\to^{}_{\beta_{!}}S$ iff $M\to^{}_{s}S^{\prime}$