Realizability in the Unitary Sphere

TL;DR

This paper introduces a realizability-based semantics for a linear algebraic lambda-calculus that characterizes unitarity, providing a foundation that extends to classical and quantum lambda-calculi.

Contribution

It presents a novel realizability semantics for linear algebraic lambda-calculus that captures unitarity and extends to classical and quantum systems.

Findings

Semantics characterizes unitarity in the system

Derived typing rules for a simply-typed linear algebraic lambda-calculus

Extension of the calculus to classical and quantum lambda-calculi

Abstract

In this paper we present a semantics for a linear algebraic lambda-calculus based on realizability. This semantics characterizes a notion of unitarity in the system, answering a long standing issue. We derive from the semantics a set of typing rules for a simply-typed linear algebraic lambda-calculus, and show how it extends both to classical and quantum lambda-calculi.

Tables

Table 1. TABLE I: Syntax of the calculus

Table 2. TABLE II: Congruence rules on term distributions

Table 3. TABLE III: Inference rules of the relation of atomic evaluation t ▷ t → ′ ▷ 𝑡 superscript → 𝑡 ′ t\mathrel{\triangleright}\vec{t}^{\prime}

$\begin{array}{c}\begin{array}{c}\\ \overline{(\lambda x.\overrightarrow{t})v▷\overrightarrow{t}[x:=v]}\end{array}\begin{array}{c}\\ \overline{\ast ;\overrightarrow{s}▷\overrightarrow{s}}\end{array}\begin{array}{c}\\ \overline{\text{let}(x,y)=(v,w)\text{in}\overrightarrow{s}▷\overrightarrow{s}\left[x:=v,y:=w\right]}\end{array}\\ \begin{array}{c}\\ \stackrel{‾}{\text{match}\text{inl}\left(v\right)\left\{\text{inl}\left(x_1\right)\mapsto {\overrightarrow{s}}_1\right|\text{inr}\left(x_2\right)\mapsto {\overrightarrow{s}}_2\}▷{\overrightarrow{s}}_1\left[x_1:=v\right]}\end{array}\begin{array}{c}\\ \stackrel{‾}{\text{match}\text{inr}\left(v\right)\left\{\text{inl}\left(x_1\right)\mapsto {\overrightarrow{s}}_1\right|\text{inr}\left(x_2\right)\mapsto {\overrightarrow{s}}_2\}▷{\overrightarrow{s}}_2\left[x_2:=v\right]}\end{array}\\ \begin{array}{c}t▷{\overrightarrow{t}}^{\prime }\\ \overline{st▷s{\overrightarrow{t}}^{\prime }}\end{array}\begin{array}{c}t▷{\overrightarrow{t}}^{\prime }\\ \overline{tv▷{\overrightarrow{t}}^{\prime }v}\end{array}\begin{array}{c}t▷{\overrightarrow{t}}^{\prime }\\ \overline{t;\overrightarrow{s}▷{\overrightarrow{t}}^{\prime };\overrightarrow{s}}\end{array}\begin{array}{c}t▷{\overrightarrow{t}}^{\prime }\\ \overline{\text{let}(x,y)=t\text{in}\overrightarrow{s}▷\text{let}(x,y)={\overrightarrow{t}}^{\prime }\text{in}\overrightarrow{s}}\end{array}\\ \begin{array}{c}t▷{\overrightarrow{t}}^{\prime }\\ \stackrel{‾}{\text{match}t\left\{\text{inl}\left(x_1\right)\mapsto {\overrightarrow{s}}_1\right|\text{inr}\left(x_2\right)\mapsto {\overrightarrow{s}}_2\}▷\text{match}{\overrightarrow{t}}^{\prime }\left\{\text{inl}\left(x_1\right)\mapsto {\overrightarrow{s}}_1\right|\text{inr}\left(x_2\right)\mapsto {\overrightarrow{s}}_2\}}\end{array}\end{array}$

Table 4. TABLE IV: Syntax of unitary types

$A,B::=𝕌\mid ♭A\mid ♯A\mid A+B\mid A\times B\mid A\to B\mid A\Rightarrow B$

Table 5. TABLE V: Unitary semantics of types

	$⟦𝕌⟧$	$:=\{\ast \}⟦♭A⟧:=♭⟦A⟧⟦♯A⟧:=\mathrm{span}\left(⟦A⟧\right)\cap {𝒮}_1$
	$⟦A+B⟧$	$:=\{\text{inl}\left(\overrightarrow{v}\right):\overrightarrow{v}\in ⟦A⟧\}\cup \{\text{inr}\left(\overrightarrow{w}\right):\overrightarrow{w}\in ⟦B⟧\}$
	$⟦A\times B⟧$	$:=\{(\overrightarrow{v},\overrightarrow{w}):\overrightarrow{v}\in ⟦A⟧,\overrightarrow{w}\in ⟦B⟧\}$
	$⟦A\to B⟧$	$:=\{\lambda x.\overrightarrow{t}:\forall \overrightarrow{v}\in ⟦A⟧,\overrightarrow{t}⟨x:=\overrightarrow{v}⟩⊩B\}$
	$⟦A\Rightarrow B⟧$	$:=\{({\sum }_{i=1}^n{\alpha }_i\cdot \lambda x.{\overrightarrow{t}}_i)\in {𝒮}_1:\forall \overrightarrow{v}\in ⟦A⟧,$
		$({\sum }_{i=1}^n{\alpha }_i\cdot {\overrightarrow{t}}_i⟨x:=\overrightarrow{v}⟩)⊩B\}$

Table 6. TABLE VI: Some valid typing rules

$\begin{array}{c}\begin{array}{cc}& \text{(Axiom)}\\ \overline{x:A⊢x:A}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:A\hspace{1em}A\le A^{\prime }& \text{(Sub)}\\ \overline{\Gamma ⊢\overrightarrow{t}:A^{\prime }}\end{array}\begin{array}{cc}\Gamma ,x:A⊢\overrightarrow{t}:B\hspace{1em}♭\Gamma \simeq \Gamma & \text{(PureLam)}\\ \overline{\Gamma ⊢\lambda x.\overrightarrow{t}:A\to B}\end{array}\begin{array}{cc}\Gamma ,x:A⊢\overrightarrow{t}:B& \text{(UnitLam)}\\ \overline{\Gamma ⊢\lambda x.\overrightarrow{t}:A\Rightarrow B}\end{array}\\ \\ \begin{array}{cc}\Gamma ⊢\overrightarrow{s}:A\Rightarrow B\hspace{1em}\Delta ⊢\overrightarrow{t}:A& \text{(App)}\\ \overline{\Gamma ,\Delta ⊢\overrightarrow{s}\overrightarrow{t}:B}\end{array}\begin{array}{cc}& \text{(Void)}\\ \overline{⊢\ast :𝕌}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:𝕌\hspace{1em}\Delta ⊢\overrightarrow{s}:A& \text{(Seq)}\\ \overline{\Gamma ,\Delta ⊢\overrightarrow{t};\overrightarrow{s}:A}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:♯𝕌\hspace{1em}\Delta ⊢\overrightarrow{s}:♯A& \text{(SeqSharp)}\\ \overline{\Gamma ,\Delta ⊢\overrightarrow{t};\overrightarrow{s}:♯A}\end{array}\\ \\ \begin{array}{cc}\Gamma ⊢\overrightarrow{v}:A\hspace{1em}\Delta ⊢\overrightarrow{w}:B& \text{(Pair)}\\ \overline{\Gamma ,\Delta ⊢(\overrightarrow{v},\overrightarrow{w}):A\times B}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:A\times B\hspace{1em}\Delta ,x:A,y:B⊢\overrightarrow{s}:C& \text{(LetPair)}\\ \overline{\Gamma ,\Delta ⊢\text{let}(x,y)=\overrightarrow{t}\text{in}\overrightarrow{s}:C}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:A\otimes B\hspace{1em}\Delta ,x:♯A,y:♯B⊢\overrightarrow{s}:♯C& \text{(LetTens)}\\ \overline{\Gamma ,\Delta ⊢\text{let}(x,y)=\overrightarrow{t}\text{in}\overrightarrow{s}:♯C}\end{array}\\ \\ \begin{array}{cc}\Gamma ⊢\overrightarrow{v}:A& \text{(InL)}\\ \overline{\Gamma ⊢\text{inl}\left(\overrightarrow{v}\right):A+B}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{w}:B& \text{(InR)}\\ \overline{\Gamma ⊢\text{inr}\left(\overrightarrow{w}\right):A+B}\end{array}\begin{array}{cc}\Gamma ⊢\overrightarrow{t}:A+B\hspace{1em}\Delta ,x_1:A⊢{\overrightarrow{s}}_1:C\hspace{1em}\Delta ,x_2:B⊢{\overrightarrow{s}}_2:C& \text{(PureMatch)}\\ \stackrel{‾}{\Gamma ,\Delta ⊢\text{match}\overrightarrow{t}\left\{\text{inl}\left(x_1\right)\mapsto {\overrightarrow{s}}_1\right|\text{inr}\left(x_2\right)\mapsto {\overrightarrow{s}}_2\}:C}\end{array}\\ \\ \begin{array}{cc}\Gamma ⊢\overrightarrow{t}:B\hspace{1em}♭A\simeq A& \text{(Weak)}\\ \overline{\Gamma ,x:A⊢\overrightarrow{t}:B}\end{array}\begin{array}{cc}\Gamma ,x:A,y:A⊢\overrightarrow{t}:B\hspace{1em}♭A\simeq A& \text{(Contr)}\\ \overline{\Gamma ,x:A⊢\overrightarrow{t}\left[y:=x\right]:B}\end{array}\end{array}$

Table 7. TABLE VII: Typing rules for λ Q subscript 𝜆 𝑄 \lambda_{Q}

$\begin{array}{c}\begin{array}{c}\\ \overline{\Delta |x:A_Q{⊢}_{Q}x:A_Q}\end{array}\begin{array}{c}\Delta |{\Gamma }_1{⊢}_{Q}s:A_Q\hspace{1em}\Delta |{\Gamma }_2{⊢}_{Q}t:B_Q\\ \overline{\Delta |{\Gamma }_1,{\Gamma }_2{⊢}_{Q}s\otimes t:A_Q\otimes B_Q}\end{array}\\ \\ \begin{array}{c}\Delta |\Gamma {⊢}_{Q}t:\mathrm{𝗊𝖻𝗂𝗍}\\ \overline{\Delta |\Gamma {⊢}_{Q}U\left(t\right):\mathrm{𝗊𝖻𝗂𝗍}}\end{array}\\ \\ \begin{array}{c}\Delta |{\Gamma }_1{⊢}_{Q}s:A_Q\otimes B_Q\hspace{1em}\Delta |{\Gamma }_2,x:A_Q,y:B_Q{⊢}_{Q}t:C_Q\\ \overline{\Delta |{\Gamma }_1,{\Gamma }_2{⊢}_Q\mathrm{𝗅𝖾𝗍}x\otimes y=s\mathrm{𝗂𝗇}t:C_Q}\end{array}\\ \\ \begin{array}{c}\Delta {⊢}_{C}t:\mathrm{𝖻𝗂𝗍}\\ \overline{\Delta |\varnothing {⊢}_Q\mathrm{𝗇𝖾𝗐}\left(t\right):\mathrm{𝗊𝖻𝗂𝗍}}\end{array}\begin{array}{c}\Delta |x:A_Q{⊢}_{Q}t:B_Q\\ \overline{\Delta {⊢}_C{\lambda }^{Q}x.t:A_Q⊸B_Q}\end{array}\\ \\ \begin{array}{c}\Delta {⊢}_{C}s:A_Q⊸B_Q\hspace{1em}\Delta |\Gamma {⊢}_{Q}t:A_Q\\ \overline{\Delta |\Gamma {⊢}_{Q}s@t:B_Q}\end{array}\end{array}$

Table 8. TABLE VIII: Operational sematics of λ Q subscript 𝜆 𝑄 \lambda_{Q}

	$[Q,L,C\left\{(\lambda x.t)u\right\}]$	$\to [Q,L,C\left\{t\left[x:=u\right]\right\}]$
	$[Q,L,C\left\{({\lambda }^{Q}x.t)@u\right\}]$	$\to [Q,L,C\left\{t\left[x:=u\right]\right\}]$
	$[Q,L,C\left\{{\pi }_1(u,v)\right\}]$	$\to [Q,L,C\left\{u\right\}]$
	$[Q,L,C\left\{{\pi }_2(u,v)\right\}]$	$\to [Q,L,C\left\{v\right\}]$
	$[Q,L,C\left\{𝚒𝚏𝚝𝚝\{t\mid r\}\right\}]$	$\to [Q,L,C\left\{t\right\}]$
	$[Q,L,C\left\{𝚒𝚏𝚏𝚏\{t\mid r\}\right\}]$	$\to [Q,L,C\left\{r\right\}]$
	$[Q,L,C\left\{\mathrm{𝗅𝖾𝗍}x\otimes y=u\otimes v\mathrm{𝗂𝗇}s\right\}]$	$\to [Q,L,C\left\{s\left[x:=u,y:=v\right]\right\}]$
	$[Q,L,C\left\{\mathrm{𝗇𝖾𝗐}\left(𝚝𝚝\right)\right\}]$	$\to [Q\otimes |0⟩,L\cup \left\{x\mapsto n+1\right\},C\left\{x\right\}]$
	$[Q,L,C\left\{\mathrm{𝗇𝖾𝗐}\left(𝚏𝚏\right)\right\}]$	$\to [Q\otimes |1⟩,L\cup \left\{x\mapsto n+1\right\},C\left\{x\right\}]$
	$[Q,L,C\left\{U\left(x\right)\right\}]$	$\to [Q^{\prime },L,C\left\{x\right\}]$
	where Q’ is obtained by applying U to the quantum bit L(x)

Equations

$$\begin{array}[]{ccc}\Lambda(\mathcal{X})&\subset&\vec{\Lambda}(\mathcal{X})\\ {\cup}&&{\cup}\\ \mathrm{V}(\mathcal{X})&\subset&\vec{\mathrm{V}}(\mathcal{X})\end{array}$$

$$\begin{array}[]{r@{\,{}\,}c@{\,{}\,}l}\lambda x\,{.}\,\vec{s}_{1}+\vec{s}_{2}&{\neq}&\lambda x\,{.}\,\vec{s}_{2}+\vec{s}_{1}\\ t;(\vec{s}_{1}+\vec{s}_{2})&{\neq}&t;(\vec{s}_{2}+\vec{s}_{1})\\ \texttt{let}~{}(x,y)=t~{}\texttt{in}~{}\vec{s}_{1}+\vec{s}_{2}&{\neq}&\texttt{let}~{}(x,y)=t~{}\texttt{in}~{}\vec{s}_{2}+\vec{s}_{1}\\ \lx@intercol\texttt{match}~{}t~{}\{\texttt{inl}(x)\mapsto\vec{s}_{1}+\vec{s}_{2}~{}|~{}\texttt{inr}(y)\mapsto\vec{s}\}\hfil\lx@intercol\\ \lx@intercol\hfil\neq\texttt{match}~{}t~{}\{\texttt{inl}(x)\mapsto\vec{s}_{2}+\vec{s}_{1}~{}|~{}\texttt{inr}(y)\mapsto\vec{s}\}\lx@intercol\\ \lx@intercol\texttt{match}~{}t~{}\{\texttt{inl}(x)\mapsto\vec{s}~{}|~{}\texttt{inr}(y)\mapsto\vec{s}_{1}+\vec{s}_{2}\}\hfil\lx@intercol\\ \lx@intercol\hfil\neq\texttt{match}~{}t~{}\{\texttt{inl}(x)\mapsto\vec{s}~{}|~{}\texttt{inr}(y)\mapsto\vec{s}_{2}+\vec{s}_{1}\}\lx@intercol\end{array}$$

$$\displaystyle\begin{aligned} \textstyle(\vec{v},\vec{w})&\textstyle:=\sum_{i=1}^{n}\sum_{j=1}^{k}\alpha_{i}\beta_{j}\cdot(v_{i},w_{j})\\ \textstyle\texttt{inl}(\vec{v})&\textstyle:=\sum_{i=1}^{n}\alpha_{i}\cdot\texttt{inl}(v_{i})\\ \textstyle\texttt{inr}(\vec{v})&\textstyle:=\sum_{i=1}^{n}\alpha_{i}\cdot\texttt{inr}(v_{i})\\ \textstyle\vec{t}\,\vec{s}&\textstyle:=\sum_{k=1}^{p}\sum_{\ell=1}^{q}\gamma_{k}\delta_{\ell}\cdot t_{k}s_{\ell}\\ \textstyle\vec{t};\vec{s}&\textstyle:=\sum_{k=1}^{p}\gamma_{k}\cdot(t_{k};\vec{s})\\ \textstyle\texttt{let}~{}(x,y)=\vec{t}~{}\texttt{in}~{}\vec{s}&\textstyle:=\sum_{k=1}^{p}\gamma_{k}\cdot\big{(}\texttt{let}~{}(x,y)=t_{k}~{}\texttt{in}~{}\vec{s}\big{)}\end{aligned}$$

$$\text{match}\vec{t}\{\text{inl}(x_1)\mapsto {\vec{s}}_1|\text{inr}(x_2)\mapsto {\vec{s}}_2\}:=$$

$$\displaystyle\textstyle\sum_{k=1}^{p}\gamma_{k}\cdot\big{(}\texttt{match}~{}t_{k}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}\big{)}$$

$$t$$

$$0\cdot Y_t=\alpha \cdot Y_t+(-\alpha )\cdot Y_t\succ \alpha \cdot (t+Y_t)+(-\alpha )\cdot Y_t=\alpha \cdot t+0\cdot Y_t$$

$$\alpha \cdot t+0\cdot Y_t\succ \alpha \cdot t+((-\alpha )\cdot t+0\cdot Y_t)=0\cdot t+0\cdot Y_t$$

$$H~{}:=~{}\lambda x\,{.}\,\mathtt{i{\mskip-1.0mu}f}~{}x~{}\Bigl{\{}~{}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{f\!f}\Bigm{|}~{}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+(-{\textstyle\frac{1}{\sqrt{2}}})\cdot\mathtt{f\!f}\Bigr{\}}\,.$$

$$H(\alpha \cdot \mathtt{t}\mathtt{t}+\beta \cdot \mathtt{f}\mathtt{f})=\alpha \cdot H\mathtt{t}\mathtt{t}+\beta \cdot H\mathtt{f}\mathtt{f}$$

$$\displaystyle\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot\mathtt{i{\mskip-1.0mu}f}~{}\mathtt{t\!t}~{}\bigl{\{}~{}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{f\!f}\bigm{|}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+\bigl{(}-{\textstyle\frac{1}{\sqrt{2}}}\bigr{)}\cdot\mathtt{f\!f}\bigr{\}}+{}$$

$$\displaystyle\hskip 17.07164pt\beta\cdot\mathtt{i{\mskip-1.0mu}f}~{}\mathtt{f\!f}~{}\bigl{\{}~{}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{f\!f}\bigm{|}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+\bigl{(}-{\textstyle\frac{1}{\sqrt{2}}}\bigr{)}\cdot\mathtt{f\!f}\bigr{\}}$$

$$\displaystyle\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot\bigl{(}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{f\!f}\bigr{)}~{}+~{}\beta\cdot\bigl{(}{\textstyle\frac{1}{\sqrt{2}}}\cdot\mathtt{t\!t}+\bigl{(}-{\textstyle\frac{1}{\sqrt{2}}}\bigr{)}\cdot\mathtt{f\!f}\bigr{)}$$

$$=\frac{1}{\sqrt{2}}(\alpha +\beta )\cdot \mathtt{t}\mathtt{t}+\frac{1}{\sqrt{2}}(\alpha -\beta )\cdot \mathtt{f}\mathtt{f}$$

$$⟨\vec{v}|\vec{w}⟩$$

$$\Vert \vec{v}\Vert$$

$$J_0\text{lx@proof@logical@and}{J}_1\cdots J_n$$

$$A,B::=\mathbb{U}\mid A+B\mid A\times B\mid A\to B$$

$$\displaystyle\textstyle\bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}$$

$$\displaystyle\textstyle\text{iff}\quad\lambda x\,{.}\,\bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\vec{t}_{i}\bigr{)}$$

$$\begin{array}[t]{@{}lll@{}}\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot\mathtt{t\!t}&\text{for some }\alpha\in\mathbb{C}\text{\,s.t.\,}|\alpha|=1,&\text{or}\\ \vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\beta\cdot\mathtt{f\!f}&\text{for some }\beta\in\mathbb{C}\text{\,s.t.\,}|\beta|=1,&\text{or}\\ \vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f}&\lx@intercol\text{for some }\alpha,\beta\in\mathbb{C}\text{\,s.t.\,}|\alpha|^{2}\,{+}\,|\beta|^{2}=1\,.\hfil\lx@intercol\end{array}$$

$$\begin{array}[]{c}\pi_{\mathbb{B}}(\alpha\cdot\mathtt{t\!t})~{}=~{}(\alpha,0),\qquad\pi_{\mathbb{B}}(\beta\cdot\mathtt{f\!f})~{}=~{}(0,\beta),\\ \text{and}\qquad\pi_{\mathbb{B}}(\alpha\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f})~{}=~{}(\alpha,\beta)\end{array}$$

$$⟨{\pi }_{\mathbb{B}}(\vec{v})|{\pi }_{\mathbb{B}}(\vec{w}){⟩}_{{\mathbb{C}}^2}=⟨\vec{v}|\vec{w}{⟩}_{\vec{\mathrm{V}}}$$

$$\vec{t}\vec{v}\succ \succ \vec{w}\text{and}{\pi }_{\mathbb{B}}(\vec{w})=F({\pi }_{\mathbb{B}}(\vec{v})).$$

$$[[\Gamma ]]$$

$$\displaystyle\qquad\text{and}~{}{}~{}\forall x\in\mathrm{dom}(\sigma),~{}\sigma(x)\in\llbracket\Gamma(x)\rrbracket\bigr{\}}\,.$$

$${\mathrm{dom}}^{♯}(\Gamma ):=\{x\in \mathrm{dom}(\Gamma ):[[\Gamma (x)]]\ne ♭[[\Gamma (x)]]\}.$$

$$A,B::=\mathbb{U}\mid A+B\mid A\times B\mid A\to B$$

$$\Gamma ⊢({\Delta }_1⊢{\vec{t}}_1)\perp ({\Delta }_2⊢{\vec{t}}_2):A$$

$$⊢(x:♯\mathbb{U}⊢x;|+⟩)\perp (y:♯\mathbb{U}⊢y;|-⟩):♯\mathbb{B}$$

$$A,B$$

$$A_Q,B_Q$$

$$t,r,s$$

$$\mid \mathtt{t}\mathtt{t}\mid \mathtt{f}\mathtt{f}\mid \mathtt{i}\mathtt{f}t\{r\mid s\}$$

$$\mid t\otimes r\mid \mathsf{let}x\otimes y=t\mathsf{in}r$$

Full text

I Introduction

The linear-algebraic lambda calculus (Lineal) [1, 2, 3] is an extension of the lambda calculus where lambda terms are closed under linear combinations over a semiring $K$. For instance, if $t$ and $r$ are two lambda terms, then so is $\alpha.t+\beta.r$ with $\alpha,\beta\in K$. The original motivation of [1] for such a calculus was to set the basis for a future quantum calculus, where $\alpha.t+\beta.r$ could be seen as the generalization of the notion of quantum superposition to the realm of programs (in which case $K$ is the field $\mathbb{C}$ of complex numbers).

In quantum computation, data is encoded in the state of a set of particles governed by the laws of quantum mechanics. The mathematical formalization postulates that quantum data is modeled as a unit vector in a Hilbert space. The quantum analogue to a Boolean value is the quantum bit, that is a linear combination of the form $\phi=\alpha|0\rangle+\beta|1\rangle$, where $|0\rangle$ and $|1\rangle$ respectively correspond to “true” and “false”, and where $|\alpha|^{2}+|\beta|^{2}=1$. In other words, the state $\phi$ is a linear combination of the Boolean values “true” and “false”, of $l_{2}$-norm equal to $1$: it is a unit-vector in the Hilbert space $\mathbb{C}^{2}$.

A quantum memory consists in a list of registers holding quantum bits. The canonical model for interacting with a quantum memory is the QRAM model [4]. A fixed set of elementary operations are allowed on each quantum register. Mathematically, these operations are modeled with unitary maps on the corresponding Hilbert spaces, that is: linear maps preserving the $l_{2}$-norm and the orthogonality. These operations, akin to Boolean gates, are referred to as quantum gates, and they can be combined into linear sequences called quantum circuits. Quantum algorithms make use of a quantum memory to solve a particular classical problem. Such an algorithm therefore consists in particular in the description of a quantum circuit.

Several existing languages for describing quantum algorithms such as Quipper [5] and QWIRE [6] are purely functional and based on the lambda calculus. However, they only provide classical control: the quantum memory and the allowed operations are provided as black boxes. These languages are mainly circuit description languages using opaque high-level operations on circuits. They do not feature quantum control, in the sense that the operations on quantum data are not programmable.

A lambda calculus with linear combinations of terms made “quantum” would allow to program those “black boxes” explicitly, and provide an operational meaning to quantum control. However, when trying to identify quantum data with linear combinations of lambda terms, the problem arises from the norm condition on quantum superpositions. To be quantum-compatible, one cannot have any linear combination of programs. Indeed, programs should at the very least yield valid quantum superpositions, that is: linear combinations whose $l_{2}$-norm equals $1$—a property which turns out to be very difficult to preserve along the reduction of programs.

So far, the several attempts at accommodating linear algebraic lambda calculi with the $l_{2}$-norm have failed. At one end of the spectrum, [7] stores lambda terms directly in the quantum memory, and encodes the reduction process as a purely quantum process. Van Tonder shows that this forces all lambda terms in superposition to be mostly equivalent. At the other end of the spectrum, the linear algebraic approaches pioneered by Arrighi and Dowek consider a constraint-free calculus and try to recover quantum-like behavior by adding ad-hoc term reductions [1] or type systems [8, 9, 10]. But if these approaches yield very expressive models of computations, none of them is managing to precisely characterize linear combinations of terms of unit $l_{2}$-norm, or equivalently, the unitarity of the representable maps.

This paper answers this question by presenting an algebraic lambda calculus together with a type system that enforces unitarity. For that, we use semantic techniques coming from realizability [11] to decide on the unitarity of terms.

Since its creation by Kleene as a semantics for Heyting arithmetic, realizability has evolved to become a versatile toolbox, that can be used both in logic and in functional programming. Roughly speaking, realizability can be seen as a generalization of the notion of typing where the relation between a term and its type is not defined from a given set of inference rules, but from the very operational semantics of the calculus, via a computational interpretation of types seen as specifications. Types are first defined as sets of terms verifying certain properties, and then, valid typing rules are derived from these properties rather than set up as axioms.

The main feature of our realizability model is that types are not interpreted as arbitrary sets of terms or values, but as subsets of the unit sphere of a particular weak vector space [3], whose vectors are distributions (i.e. weak linear combinations) of “pure” values. So that by construction, all functions that are correct w.r.t. this semantics preserve the $\ell_{2}$-norm. As we shall see, this interpretation of types is not only compatible with the constructions of the simply typed lambda calculus (with sums and pairs), but it also allows us to distinguish pure data types (such as the type $\mathbb{B}$ of pure Booleans) from quantum data types (such as the type $\sharp\mathbb{B}$ of quantum Booleans). Thanks to these constraints, the type system we obtain naturally enforces that the realizers of the type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ are precisely the functions representing unitary operators of $\mathbb{C}^{2}$.

This realizability model is therefore answering a hard problem [12]: it provides a unifying framework able to express not only classical control, with the presence of “pure” values, but also quantum control, with the possibility to interpret quantum data-types as (weak) linear combinations of classical ones.

I-A Contributions

(1) We propose a realizability semantics based on a linear algebraic lambda calculus capturing a notion of unitarity through the use of a $l_{2}$-norm. As far as we know, such a construction is novel.

(2) The semantics provides a unified model for both classical and quantum control. Strictly containing the simply-typed lambda calculus, it does not only serve as a model for a quantum circuit-description language, but it also provides a natural interpretation of quantum control.

(3) In order to exemplify the expressiveness of the model, we show how a circuit-description language in the style of QWIRE [6] can be naturally interpreted in the model. Furthermore, we discuss how one can give within the model an operational semantics to a high-level operation on circuits usually provided as a black box in circuit-description languages: the control of a circuit.

I-B Related Works

Despite its original motivations, [10] showed that Lineal can handle the $l_{1}$-norm. This can be used for example to represent probabilistic distributions of terms. Also, a simplification of Lineal, without scalars, can serve as a model for non-deterministic computations [13]. And, in general, if we consider the standard values of the lambda calculus as the basis, then linear combinations of those form a vector space, which can be characterized using types [9]. In [14] a similar distinction between classical bits ($\mathbb{B}$) and qbits ($\sharp\mathbb{B}$) has been also studied. However, without unitarity, it is impossible to obtain a calculus that could be compiled onto a quantum machine. Finally, a concrete categorical semantics for such a calculus has been recently given in [15].

An alternative approach for capturing unitarity (of data superpositions and functions) consists to change the language. Instead of starting with a lambda calculus, [16] defines and extends a reversible language to express quantum computation.

Lambda calculi with vectorial structures are not specific to quantum computation. Vaux [17] independently developed the algebraic lambda calculus (where linear combinations of terms are also terms), initially to study a fragment of the differential lambda calculus of [18]. Unlike its quantum-inspired cousin Lineal, the algebraic lambda calculus is morally call-by-name, and [19] shows the formal connection with Lineal.

Designing an (unconstrainted) algebraic lambda calculus (in call-by-name [17] or in call-by-value [1]) raises the problem of how to enforce the confluence of reduction. Indeed, if the semi-ring $K$ is a ring, since $0\cdot t=\vec{0}$, it is possible to design a term $Y_{t}$ reducing both to $t$ and the empty linear combination $\vec{0}$. A simple solution to recover consistency is to weaken the vectorial structure and remove the equality $0\cdot{t}=\vec{0}$ [3]. The vector space of terms becomes a weak vector space. This approach is the one we shall follow in our construction.

This paper is concerned with modeling quantum higher-order programming languages. If the use of realizability techniques is novel, several other techniques have been used, based on positive matrices and categorical tools. For first-order quantum languages, [20] constructs a fully complete semantics based on superoperators. To model a strictly linear quantum lambda-calculus, [21] shows that the compact closed category CPM based on completely positive maps forms a fully abstract model. Another approach has been taken in [22], with the use of a presheaf model on top of the category of superoperators. To accomodate duplicable data, [23] extends CPM using techniques developed for quantitative models of linear logic. Finally, a categorical semantics of circuit-description languages has been recently designed using linear-non-linear models by [24, 25].

I-C Outline

Section II presents the linear algebraic calculus and its weak vector space structure. Section III discusses the evaluation of term distributions. Section IV introduces the realizability semantics and the algebra of types spawning from it. At the end of this section, Theorem IV.12 and Corollary IV.13 express that the type of maps from quantum bits to quantum bits only contains unitary functions. Section V introduces a notion of typing judgment and derives a set of valid typing rules from the semantics. Section V-B discusses the inclusion of the simply-typed lambda calculus in this unitary semantics. Finally, Section VI describes a small quantum circuit-description language and shows how it lives inside the unitary semantics.

II Syntax of the calculus

This section presents the calculus upon which our realizability model will be designed. It is a lambda-calculus extended with linear combinations of lambda-terms, but with a subtelty: terms form a weak vector space.

II-A Values, terms and distributions

The language is made up of four syntactic categories: pure values, pure terms, value distributions and term distributions (Table I). As usual, the expressions of the language are built from a fixed denumerable set of variables, written $\mathcal{X}$.

In this language, a pure value is either a variable $x$, a $\lambda$-abstraction $\lambda x\,{.}\,\vec{s}$ (whose body is an arbitrary term distribution $\vec{s}$), the void object $*$, a pair of pure values $(v_{1},v_{2})$, or one the two variants $\texttt{inl}(v)$ and $\texttt{inr}(v)$ (where $v$ is pure value). A pure term is either a pure value $v$ or a destructor, that is: an application $s\,t$, a sequence  $t;\vec{s}$  for destructing the void object in $t$111Note the asymmetry: $t$ is a pure term whereas $\vec{s}$ is a term distribution. As a matter of fact, the sequence $t;\vec{s}$ (that could also be written $\texttt{let}~{}*=t~{}\texttt{in}~{}\vec{s}$) is the nullary version of the pair destructing let  $\texttt{let}~{}(x_{1},x_{2})=t~{}\texttt{in}~{}\vec{s}$., a let-construct  $\texttt{let}~{}(x_{1},x_{2})=t~{}\texttt{in}~{}\vec{s}$  for destructing a pair in $t$, or a match-construct  $\texttt{match}~{}t~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}$ (where $\vec{s}$, $\vec{s}_{1}$ and $\vec{s}_{2}$ are arbitrary term distributions). A term distribution is simply a formal $\mathbb{C}$-linear combination of pure terms, whereas a value distribution is a term distribution that is formed only from pure values. We also define Booleans using the following abbreviations: $\mathtt{t\!t}:=\texttt{inl}(*)$, $\mathtt{f\!f}:=\texttt{inr}(*)$, and, finally, $\mathtt{i{\mskip-1.0mu}f}~{}t~{}\{\vec{s}_{1}\mid\vec{s}_{2}\}:=\texttt{match}~{}t~{}\{\texttt{inl}(x_{1})\mapsto x_{1};\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto x_{2};\vec{s}_{2}\}$.

The notions of free and bound (occurrences of) variables are defined as expected, and in what follows, we shall consider pure values, pure terms, value distributions and term distributions up to $\alpha$-conversion, silently renaming bound variables whenever needed. The set of all pure terms (resp. of all pure values) is written $\Lambda(\mathcal{X})$ (resp. $\mathrm{V}(\mathcal{X})$), whereas the set of all term distributions (resp. of all value distributions) is written $\vec{\Lambda}(\mathcal{X})$ (resp. $\vec{\mathrm{V}}(\mathcal{X})$). So that we have the inclusions:

[TABLE]

II-B Distributions as weak linear combinations

Formally, the set $\vec{\Lambda}(\mathcal{X})$ of term distributions is equipped with a congruence $\equiv$ that is generated from the 7 rules of Table II.

We assume that the congruence $\equiv$ is shallow, in the sense that it only goes through sums ($+$) and scalar multiplications ($\cdot$), and stops at the level of pure terms. So that $\vec{t}+(\vec{s}_{1}+\vec{s}_{2})~{}\equiv~{}\vec{t}+(\vec{s}_{2}+\vec{s}_{1})$ but $\lambda x\,{.}\,\vec{s}_{1}+\vec{s}_{2}~{}\not\equiv~{}\lambda x\,{.}\,\vec{s}_{2}+\vec{s}_{1}$. (This important design choice will be justified in Section V-A, Remark V.5). We easily check that:

Lemma II.1**.**

For all $\alpha\in\mathbb{C}$, we have $\alpha\cdot\vec{0}\equiv\vec{0}$.

Proof.

From $0\cdot\vec{0}\equiv 0\cdot\vec{0}+\vec{0}\equiv 0\cdot\vec{0}+1\cdot\vec{0}\equiv(0+1)\cdot\vec{0}=1\cdot\vec{0}\equiv\vec{0}$, we get $\alpha\cdot\vec{0}\equiv\alpha\cdot(0\cdot\vec{0})\equiv(0\alpha)\cdot\vec{0}=0\cdot\vec{0}\equiv\vec{0}$. ∎

On the other hand, the relation $0\cdot\vec{t}\equiv\vec{0}$ cannot be derived from the rules of Table II as we shall see below (Proposition II.6 and Example II.7). As a matter of fact, the congruence $\equiv$ implements the equational theory of a restricted form of linear combinations—which we shall call distributions—that is intimately related to the notion of weak vector space [3].

Definition II.2** (Weak vector space).**

A weak vector space (over a given field $K$) is a commutative monoid $(V,{+},\vec{0})$ equipped with a scalar multiplication $({\cdot}):K\times V\to V$ such that for all $u,v\in V$, $\alpha,\beta\in K$, we have $1\cdot u=u$, $\alpha\cdot(\beta\cdot u)=\alpha\beta\cdot u$, $(\alpha+\beta)\cdot u=\alpha\cdot u+\beta\cdot u$, and $\alpha\cdot(u+v)=\alpha\cdot u+\alpha\cdot v$.

Remark II.3**.**

The notion of weak vector space differs from the traditional notion of vector space in that the underlying additive structure $(V,{+},\vec{0})$ may be an arbitrary commutative monoid, whose elements do not necessarily have an an additive inverse. So that in a weak vector space, the vector $(-1)\cdot u$ is in general not the additive inverse of $u$, and the product $0\cdot u$ does not simplify to $\vec{0}$.

Weak vector spaces naturally arise in functional analysis as the spaces of unbounded operators. Historically, the notion of unbounded operator was introduced by von Neumann to give a rigorous mathematical definition to the operators that are used in quantum mechanics. Given two (usual) vector spaces $\mathscr{E}$ and $\mathscr{F}$ (over the same field $K$), recall that an unbounded operator from $\mathscr{E}$ to $\mathscr{F}$ is a linear map $f:D(f)\to\mathscr{F}$ that is defined on a sub-vector space $D(f)\subseteq\mathscr{E}$, called the domain of $f$. The sum of two unbounded operators $f,g:\mathscr{E}\rightharpoonup\mathscr{F}$ is defined by: $D(f+g):=D(f)\cap D(g)$, $(f+g)(x):=f(x)+g(x)$ (for all $x\in D(f+g)$), whereas the product of an unbounded operator $f:\mathscr{E}\rightharpoonup\mathscr{F}$ by a scalar $\alpha\in K$ is defined by: $D(\alpha\cdot f):=D(f)$, $(\alpha\cdot f)(x):=\alpha\cdot f(x)$ (for all $x\in D(\alpha\cdot f)$).

Example II.4**.**

The space $\textrm{\L}(\mathscr{E},\mathscr{F})$ of all unbounded operators from $\mathscr{E}$ to $\mathscr{F}$ is a weak vector space, whose null vector is the (totally defined) null function.

Indeed, we observe that an unbounded operator $f\in\textrm{\L}(\mathscr{E},\mathscr{F})$ has an additive inverse if and only $f$ is total, that is: if and only if $D(f)=\mathscr{E}$—and in this case, the additive inverse of $f$ is the operator $(-1)\cdot f$. In particular, it should be clear to the reader that $0\cdot f~{}({=}~{}\vec{0}_{\restriction{D(f)}})\neq\vec{0}$ as soon as $D(f)\neq\mathscr{E}$.

We can now observe that, by construction:

Proposition II.5**.**

The space $\vec{\Lambda}(\mathcal{X})/{\equiv}$ of all term distributions (modulo the congruence $\equiv$) is the free weak $\mathbb{C}$-vector space generated by the set $\Lambda(\mathcal{X})$ of all pure terms222The same way as the space of linear combinations over a given set $X$ is the free vector space generated by $X$.. ∎

Again, the notion of distribution (or weak linear combination) differs from the standard notion of linear combination in that the summands of the form $0\cdot t$ cannot be erased, so that the distribution $t_{1}+(-3)\cdot t_{2}$ is not equivalent to the distribution $t_{1}+(-3)\cdot t_{2}+0\cdot t_{3}$ (provided $t_{3}\not\equiv t_{1},t_{2}$). In particular, the distribution $(-1)\cdot t_{1}+3\cdot t_{2}$ is not the additive inverse of $t_{1}+(-3)\cdot t_{2}$, since \bigl{(}t_{1}+(-3)\cdot t_{2}\bigr{)}+\bigl{(}(-1)\cdot t_{1}+3\cdot t_{2}\bigr{)}~{}\equiv~{}0\cdot t_{1}+0\cdot t_{2}~{}\not\equiv~{}\vec{0}\,. However, the equivalence of term distributions can be simply characterized as follows:

Proposition II.6** (Canonical form of a distribution).**

Each term distribution $\vec{t}$ can be written $\textstyle\vec{t}~{}\equiv~{}\sum_{i=1}^{n}\alpha_{i}\cdot t_{i}\,,$ where $\alpha_{1},\ldots,\alpha_{n}\in\mathbb{C}$ are arbitrary scalars (possibly equal to [math]), and where $t_{1},\ldots,t_{n}$ ($n\geq 0$) are pairwise distinct pure terms. This writing—which is called the canonical form of $\vec{t}$—is unique, up to a permutation of the summands $\alpha_{i}\cdot t_{i}$ ($i=1..n$).∎

Example II.7**.**

Given distinct pure terms $t_{1}$ and $t_{2}$, we consider the term distributions $\vec{t}:=3\cdot t_{1}$ and $\vec{t}^{\prime}:=3\cdot t_{1}+0\cdot t_{2}$. We observe that the distributions $\vec{t}$ and $\vec{t}^{\prime}$ (that are given in canonical form) do not have the same number of summands, hence they are not equivalent: $\vec{t}\not\equiv\vec{t}^{\prime}$.

Corollary II.8**.**

The congruence $\equiv$ is trivial on pure terms:  $t\equiv t^{\prime}$ iff $t=t^{\prime}$, for all $t,t^{\prime}\in\Lambda(\mathcal{X})$.∎

Thanks to Proposition II.6, we can associate to each term distribution $\vec{t}\equiv\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$ (written in canonical form) its domain $\mathrm{dom}(\vec{t}\,):=\{t_{1},\ldots,t_{n}\}$333Note that the domain of a distribution $\vec{t}\equiv\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$ gathers all pure terms $t_{i}$ ($i=1..n$), including those affected with a coefficient $\alpha_{i}=0$. So that the domain of a distribution should not be mistaken with its support. and its weight $\varpi(\vec{t}\,):=\sum_{i=1}^{n}\alpha_{i}$. Note that the weight function  $\varpi:\vec{\Lambda}(\mathcal{X})/{\equiv}\to\mathbb{C}$  is a linear function from the weak $\mathbb{C}$-vector space of term distributions to $\mathbb{C}$, whereas the domain function  $\mathrm{dom}:\vec{\Lambda}(\mathcal{X})/{\equiv}\to\mathfrak{P}_{\text{fin}}(\Lambda(\mathcal{X}))$  is a morphism of commutative monoids from $(\vec{\Lambda}(\mathcal{X})/{\equiv},{+},\vec{0})$ to $(\mathfrak{P}_{\text{fin}}(\Lambda(\mathcal{X})),{\cup},\varnothing)$, since we have444Actually, the function  $\mathrm{dom}:\vec{\Lambda}(\mathcal{X})/{\equiv}\to\mathfrak{P}_{\text{fin}}(\Lambda(\mathcal{X}))$  is even linear, since the commutative (and idempotent) monoid $(\mathfrak{P}_{\text{fin}}(\Lambda(\mathcal{X})),{\cup},\varnothing)$ has a natural structure of weak $\mathbb{C}$-vector space whose (trivial) scalar multiplication is defined by $\alpha\cdot X=X$ for all $\alpha\in\mathbb{C}$ and $X\in\mathfrak{P}_{\text{fin}}(\Lambda(\mathcal{X}))$.: $\mathrm{dom}(\vec{0})=\varnothing$, $\mathrm{dom}(\vec{t}_{1}+\vec{t}_{2})=\mathrm{dom}(\vec{t}_{1})\cup\mathrm{dom}(\vec{t}_{2})$, $\mathrm{dom}(t)=\{t\}$ and $\mathrm{dom}(\alpha\cdot\vec{t}\,)=\mathrm{dom}(\vec{t}\,)$ for all $t\in\Lambda(\mathcal{X})$, $\vec{t}_{1},\vec{t}_{2}\in\vec{\Lambda}(\mathcal{X})$ and $\alpha\in\mathbb{C}$.

Remark II.9**.**

In practice, one of the main difficulties of working with distributions is that addition is not regular, in the sense that the relation $\vec{t}+\vec{t}_{1}\equiv\vec{t}+\vec{t}_{2}$ does not necessarily imply that $\vec{t}_{1}\equiv\vec{t}_{2}$. However, for example if $\vec{t}=\alpha.s$, we can deduce that $\vec{t}_{1}\equiv\vec{t}_{2}$ or $\vec{t}_{1}\equiv\vec{t}_{2}+0\cdot s$ or $\vec{t}_{2}\equiv\vec{t}_{1}+0\cdot s$.

To simplify the notation, we shall adopt the following:

Convention II.10**.**

From now on, we consider term distributions modulo the congruence $\equiv$, and simply write $\vec{t}=\vec{t}^{\prime}$ for $\vec{t}\equiv\vec{t}^{\prime}$. This convention does not affect inner—or raw—distributions (which occur within a pure term, for instance in the body of an abstraction), that are still considered only up to $\alpha$-conversion555Intuitively, a distribution that appears in the body of an abstraction (or in the body of a let-construct, or in a branch of a match-construct) does not represent a real superposition, but it only represents machine code that will produce later a particular superposition, after some substitution has been performed.. The same convention holds for value distributions.

To sum up, we now consider that $\vec{s}_{1}+\vec{s}_{2}=\vec{s}_{2}+\vec{s}_{1}$ (as a top-level distribution), but:

[TABLE]

II-C Extending syntactic constructs by linearity

Pure terms and term distributions are intended to be evaluated according to the call-by-basis strategy (Section III), that can be seen as the declination of the call-by-value strategy in a computing environment where all functions are linear by construction. Keeping this design choice in mind, it is natural to extend the syntactic constructs of the language by linearity, proceeding as follows: for all value distributions $\vec{v}=\sum_{i=1}^{n}\alpha_{i}\cdot{v_{i}}$ and $\vec{w}=\sum_{j=1}^{m}\beta_{j}\cdot{w_{j}}$, and for all term distributions $\vec{s}_{1},\vec{s}_{2}$, $\vec{t}=\sum_{k=1}^{p}\gamma_{k}\cdot t_{k}$ and $\vec{s}=\sum_{\ell=1}^{q}\delta_{\ell}\cdot s_{\ell}$ we have:

[TABLE]

The value distribution $(\vec{v},\vec{w})$ will be sometimes written $\vec{v}\otimes\vec{w}$ as well.

II-D Substitutions

Given a variable $x$ and a pure value $w$, we define an operation of pure substitution, written $[x:=w]$, that associates to each pure value $v$ (resp. to each pure term $t$, to each raw value distribution $\vec{v}$, to each raw term distribution $\vec{t}$) a pure value $v[x:=w]$ (resp. a pure term $t[x:=w]$, a raw value distribution $\vec{v}[x:=w]$, a raw term distribution $\vec{t}[x:=w]$). The four operations $v[x:=w]$, $t[x:=w]$, $\vec{v}[x:=w]$ and $\vec{t}[x:=w]$ are defined by mutual recursion as expected.

Although the operation $\vec{t}[x:=w]$ is primarily defined on raw term distributions (i.e. by recursion on the tree structure of $\vec{t}$, without taking into account the congruence $\equiv$), it is compatible with the congruence $\equiv$, in the sense that if $\vec{t}\equiv\vec{t}^{\prime}$, then $\vec{t}[x:=w]\equiv\vec{t}^{\prime}[x:=w]$ for all pure values $w$. In other words, the operation of pure substitution is compatible with Convention II.10. It is also clear that, by construction, the operation $\vec{t}\,[x:=w]$ is linear w.r.t. $\vec{t}$, so that $\textstyle\vec{t}\,[x:=w]$ is $\sum_{i=1}^{n}\alpha_{i}\cdot t_{i}[x:=w]$ for all term distributions $\vec{t}=\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$. (The same observations hold for the operation $\vec{v}[x:=w]$).

Moreover, the operation of pure substitution behaves well with the linear extension of the syntactic constructs of the language (cf. Appendix -D). And we have the expected substitution lemma: For all term distributions $\vec{t}$ and for all pure values $v$ and $w$, provided $x\neq y$ and $x\notin\textit{FV}(w))$, we have $\vec{t}\,[x:=v][y:=w]~{}:=~{}\vec{t}\,[y:=w][x:=v[y:=w]]$. We extend the notation to parallel substitution in the usual manner (cf. Remark .14 in Appendix -D).

From the operation of pure substitution $[x:=w]$, we define an operation of bilinear substitution $\langle x:=\vec{w}\,\rangle$ that is defined for all term distributions $\vec{t}=\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$ and for all value distributions $\vec{w}=\sum_{j=1}^{m}\beta_{j}\cdot{w_{j}}$, letting $\textstyle\vec{t}\langle x:=\vec{w}\,\rangle~{}:=~{}\sum_{j=1}^{m}\beta_{j}\cdot\vec{t}\,[x:=w_{j}]~{}=~{}\sum_{i=1}^{n}\sum_{j=1}^{m}\alpha_{i}\beta_{j}\cdot t_{i}[x:=w_{j}]\,.$ By construction, the generalized operation of substitution $\vec{t}\langle x:=\vec{w}\rangle$ is bilinear—which is consistent with the bilinearity of application (Section II-C). But beware! The bilinearity of the operation $\vec{t}\langle x:=\vec{w}\rangle$ also makes its use often counter-intuitive, so that this notation should always be used with the greatest caution. Indeed, while $\texttt{inl}(\vec{v})\langle x:=\vec{w}\rangle=\texttt{inl}(\vec{v}\langle x:=\vec{w}\rangle)$, $(v_{1},v_{2})\langle x:=\vec{w}\rangle\neq(v_{1}\langle x:=\vec{w}\rangle,v_{2}\langle x:=\vec{w}\rangle)$. Lemma .10, in Appendix -C gives the valid identities. In addition, bilinear substitution is not (completely) canceled when $x\notin\textit{FV}(\vec{t})$, in which case $\vec{t}\langle x:=\vec{w}\rangle=\varpi(\vec{w})\cdot\vec{t}\quad\neq\quad\vec{t}$. where $\varpi(\vec{w}):=\sum_{j=1}^{m}\beta_{j}$ is the weight of $\vec{w}$ (cf Section II-B).

III Evaluation

The set of term distributions is equipped with a relation of evaluation $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$ that is defined in three steps as follows.

III-A Atomic evaluation

First we define an asymmetric relation of atomic evaluation $t\mathrel{\triangleright}\vec{t}^{\prime}$ (between a pure term $t$ and a term distribution $\vec{t}^{\prime}$) from the inference rules of Table III.

These rules basically implement a deterministic call-by-value strategy, where function arguments are evaluated from the right to the left. (The argument of an application is always evaluated before the function666This design choice is completely arbitrary, and we could have proceeded the other way around.). Also notice that no reduction is ever performed in the body of an abstraction, in the second argument of a sequence, in the body of a let-construct, or in a branch of a match-construct. Moreover, atomic evaluation is substitutive: If $t\mathrel{\triangleright}\vec{t}^{\prime}$, then $t[x:=w]\mathrel{\triangleright}\vec{t}^{\prime}[x:=w]$ for all pure values $w$.

III-B One step evaluation

The relation of one step evaluation $\vec{t}\succ\vec{t}^{\prime}$ is defined as follows:

Definition III.1** (One step evaluation).**

Given two term distributions $\vec{t}$ and $\vec{t}^{\prime}$, we say that $\vec{t}$ evaluates in one step to $\vec{t}^{\prime}$ and write $\vec{t}\succ\vec{t}^{\prime}$ when there exist a scalar $\alpha\in\mathbb{C}$, a pure term $s$ and two term distributions $\vec{s^{\prime}}$ and $\vec{r}$ such that $\vec{t}=\alpha\cdot s+\vec{r}$, $\vec{t}^{\prime}=\alpha\cdot\vec{s^{\prime}}+\vec{r}$, and $s\mathrel{\triangleright}\vec{s^{\prime}}$.

Notice that the relation of one step evaluation is also substitutive. In addition, the strict determinism of the relation of atomic evaluation $t\mathrel{\triangleright}\vec{t}^{\prime}$ implies that the relation of one step evaluation fulfills the following weak diamond property:

Lemma III.2** (Weak diamond).**

If $\vec{t}\succ\vec{t}^{\prime}_{1}$ and $\vec{t}\succ\vec{t}^{\prime}_{2}$, then one of the following holds: either $\vec{t}^{\prime}_{1}=\vec{t}^{\prime}_{2}$; either $\vec{t}^{\prime}_{1}\succ\vec{t}^{\prime}_{2}$ or $\vec{t}^{\prime}_{2}\succ\vec{t}^{\prime}_{1}$; either $\vec{t}^{\prime}_{1}\succ\vec{t^{\prime\prime}}$ and $\vec{t}^{\prime}_{2}\succ\vec{t^{\prime\prime}}$ for some $\vec{t^{\prime\prime}}$.∎

Remark III.3**.**

In the decomposition  $\vec{t}=\alpha\cdot{s}+\vec{r}$  of Definition III.1, we allow that $s\in\mathrm{dom}(\vec{r})$. So that for instance, we have the following. Let $t:=(\lambda x\,{.}\,x)\,y$. Then,

[TABLE]

Remark III.4**.**

Given a pure term $t$, we write  $Y_{t}:=(\lambda x\,{.}\,t+xx)(\lambda x\,{.}\,t+xx)$,  so that we have $Y_{t}\mathrel{\triangleright}t+Y_{t}$ by construction. Then we observe that for all $\alpha\in\mathbb{C}$, we have

[TABLE]

This example does not jeopardize the confluence of evaluation, since we also have

[TABLE]

III-C Evaluation

Finally, the relation of evaluation $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$ is defined as the reflexive-transitive closure of the relation of one step evaluation $\vec{t}\succ\vec{t}^{\prime}$, that is: $({\mathrel{{\succ}\mskip-6.0mu{\succ}}}):=({\succ})^{*}$.

Proposition III.5** (Linearity of evaluation).**

The relation $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$ is linear, in the sense that:

$\vec{0}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{0}$** 2. 2.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\alpha\cdot\vec{t}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\alpha\cdot\vec{t}^{\prime}$  for all $\alpha\in\mathbb{C}$. 3. 3.

If  $\vec{t}_{1}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}_{1}$  and  $\vec{t}_{2}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}_{2}$,  then  $\vec{t}_{1}+\vec{t}_{2}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\vec{t}^{\prime}_{1}+\vec{t}^{\prime}_{2}$. ∎

Example III.6**.**

In our calculus, the Hadamard operator $H:\mathbb{C}^{2}\to\mathbb{C}^{2}$, whose matrix is given by $\mathrm{Mat}(H):={\textstyle\frac{1}{\sqrt{2}}}\left(\begin{smallmatrix}1&\hphantom{+}1\\ 1&-1\end{smallmatrix}\right)$, is computed by the term

[TABLE]

Indeed, for all $\alpha,\beta\in\mathbb{C}$, we have

[TABLE]

Theorem III.7** (Confluence of evaluation).**

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}_{1}$  and  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}_{2}$,  then there is a term distribution $\vec{t^{\prime\prime}}$ such that  $\vec{t}^{\prime}_{1}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t^{\prime\prime}}$  and  $\vec{t}^{\prime}_{2}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t^{\prime\prime}}$.

Proof.

Writing $({\succ^{?}})$ the reflexive closure of $({\succ})$, it is clear from Lemma III.2 that $({\succ^{?}})$ fulfills the diamond property. Therefore, $({\mathrel{{\succ}\mskip-6.0mu{\succ}}})=({\succ})^{*}=({\succ^{?}})^{+}$ fulfills the diamond property. ∎

III-D Normal forms

From what precedes, it is clear that the normal forms of the relation of evaluation $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$ are the term distributions of the form $\textstyle\vec{t}~{}=~{}\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$ where $t_{i}\mathrel{\not\triangleright}$ for each $i=1..n$. In particular, all value distributions $\vec{v}$ are normal forms (but they are far from being the only normal forms in the calculus). From the property of confluence, it is also clear that when a term distribution $\vec{t}$ reaches a normal form $\vec{t}^{\prime}$, then this normal form is unique.

In what follows, we shall be more particularly interested in the closed term distributions $\vec{t}$ that reach a (unique) closed value distribution $\vec{v}$ through the process of evaluation.

IV A semantic type system

In this section, we present the type system associated with the (untyped) language presented in Section II as well as the corresponding realizability semantics.

IV-A Structuring the space of value distributions

In what follows, we write: $\Lambda$ the set of all closed pure terms; $\vec{\Lambda}$ the space of all closed term distributions; $\mathrm{V}~{}({\subseteq}~{}\Lambda)$ the set of all closed pure values, which we shall call basis vectors; and $\vec{\mathrm{V}}~{}({\subseteq}~{}\vec{\Lambda})$ the space of all closed value distributions, which we shall call vectors.

The space $\vec{\mathrm{V}}$ formed by all closed value distributions (i.e. vectors) is equipped with the inner product $\langle{\vec{v}}~{}|~{}{\vec{w}}\rangle$ and the pseudo-$\ell_{2}$-norm $\|\vec{v}\,\|$ that are defined by

[TABLE]

where $\vec{v}=\sum_{i=1}^{n}\alpha_{i}\cdot v_{i}$ and $\vec{w}=\sum_{j=1}^{m}\beta_{j}\cdot w_{j}$ (both in canonical form), and where $\delta_{v_{i},w_{j}}$ is the Kronecker delta such that it is $1$ if $v_{i}=w_{j}$ and [math] otherwise. Let us observe that the inner product behaves well with term constructors, so that e.g. $\langle{\texttt{inl}(\vec{v}_{1})}~{}|~{}{\texttt{inl}(\vec{v}_{2})}\rangle=\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle$, and that values built from distinct term constructors are orthogonal, so that e.g. $\langle{\texttt{inl}(\vec{v}_{1})}~{}|~{}{\texttt{inr}(\vec{w}_{2})}\rangle=0$. We can also infer that for all $\vec{v},\vec{w}\in\vec{\mathrm{V}}$, we have $\|\texttt{inl}(\vec{v})\|=\|\texttt{inr}(\vec{v})\|=\|\vec{v}\|$  and  $\|(\vec{v},\vec{w})\|=\|\vec{v}\|\,\|\vec{w}\|$.

Most of the constructions we shall perform hereafter will take place in the unit sphere $\mathcal{S}_{1}\subseteq\vec{\mathrm{V}}$, that is defined by $\mathcal{S}_{1}:=\{\vec{v}\in\vec{\mathrm{V}}~{}:~{}\|\vec{v}\,\|=1\}$. It is clear that for all $\vec{v},\vec{w}\in\mathcal{S}_{1}$, we have $\texttt{inl}(\vec{v})\in\mathcal{S}_{1}$, $\texttt{inr}(\vec{w})\in\mathcal{S}_{1}$ and $(\vec{v},\vec{w})\in\mathcal{S}_{1}$.

Given a set of vectors $X\subseteq\vec{\mathrm{V}}$, we also write $\mathrm{span}(X)$ the span of $X$, defined by \Bigl{\{}\sum_{i=1}^{n}\alpha_{i}\cdot\vec{v}_{i}~{}:~{}n\geq 0,~{}\alpha_{1},\ldots,\alpha_{n}\in\mathbb{C},~{}\vec{v}_{1},\ldots,\vec{v}_{n}\in X\Bigr{\}}\subseteq\vec{\mathrm{V}}, and $\flat{X}$ the basis of $X$, defined by $\bigcup_{\vec{v}\in X}\mathrm{dom}(\vec{v}\,)\subseteq~{}\mathrm{V}$.

Note that by construction, $\mathrm{span}(X)$ is the smallest (weak) sub-vector space of $\vec{\mathrm{V}}$ such that $X\subseteq\mathrm{span}(X)$, whereas $\flat{X}$ is the smallest set of basis vectors such that $X\subseteq\mathrm{span}(\flat{X})$.

IV-B The notion of unitary type

Definition IV.1** (Unitary types).**

A unitary type (or a type, for short) is defined by a notation $A$, together with a set of unitary vectors $\llbracket A\rrbracket\subseteq\mathcal{S}_{1}$, called the unitary semantics of $A$.

Definition IV.2** (Realizability predicate).**

To each type $A$ we associate a realizability predicate $\vec{t}\Vdash A$ (where $\vec{t}$ ranges over $\vec{\Lambda}$) that is defined by $\vec{t}\Vdash A$ if and only if $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}$ for some $\vec{v}\in\llbracket A\rrbracket$. The set or realizers of $A$, written $\{{\Vdash}~{}A\}$, is then defined by $\{\vec{t}\in\vec{\Lambda}~{}:~{}\vec{t}\Vdash A\}$, that is, $\{\vec{t}\in\vec{\Lambda}~{}:~{}\exists\vec{v}\in\llbracket A\rrbracket,~{}\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}\}$.

Lemma IV.3**.**

For all types $A$, we have $\llbracket A\rrbracket=\{{\Vdash}~{}A\}\cap\vec{\mathrm{V}}$.∎

IV-C Judgments, inference rules and derivations

Definition IV.4** (Judgments).**

A judgment is a notation $J$ expressing some assertion, together with a criterion of validity, that defines whether the judgment $J$ is valid or not.

For instance, given any two types $A$ and $B$, we can consider the following two judgments:

• •

The judgment $A\leq B$ (‘$A$ is a subtype of $B$’), that is valid when $\llbracket A\rrbracket\subseteq\llbracket B\rrbracket$.

• •

The judgment $A\simeq B$ (‘$A$ is equivalent to $B$’), that is valid when $\llbracket A\rrbracket=\llbracket B\rrbracket$.

(In Section V-A below, we shall also introduce a typing judgment written $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A$). From the definition of both judgments $A\leq B$ and $A\simeq B$, it is clear that the judgment $A\simeq B$ is valid if and only if both judgments $A\leq B$ and $B\leq A$ are valid. Moreover:

Lemma IV.5**.**

Given any two types $A$ and $B$:

$A\leq B$* is valid if and only if $\{{\Vdash}~{}A\}\subseteq\{{\Vdash}~{}B\}$.* 2. 2.

$A\simeq B$* is valid if and only if $\{{\Vdash}~{}A\}=\{{\Vdash}~{}B\}$. ∎*

More generally, we call an inference rule any pair formed by a finite set of judgments $J_{1},\ldots,J_{n}$, called the premises of the rule, and a judgment $J_{0}$, called the conclusion:

[TABLE]

We say that an inference rule  $\frac{J_{1}~{}\cdots~{}J_{n}}{J_{0}}$  is valid when the joint validity of the premises $J_{1},\ldots,J_{n}$ implies the validity of the conclusion $J_{0}$. As usual, inference rules can be assembled into derivations, and we shall say that a derivation is valid when all the inference rules that are used to build this derivation are valid. It is clear that when all the premises of a valid derivation are valid, then so is its conclusion. In particular, when a judgment has a valid derivation without premises, then this judgment is valid.

IV-D A simple algebra of types

In this section, we design a simple algebra of unitary types whose notations (i.e. the syntax) are given in Table IV and whose unitary semantics are given in Table V.

The choice we make in this paper follows from the structure of the calculus: each set of standard constructor/destructor canonically yields a type constructor: this gives : $\mathbb{U}$, the unit type, that is inhabited by the sole vector $*$ ; $A+B$, the simple sum of $A$ and $B$ ; $A\times B$, the simple product of $A$ and $B$; $A\rightarrow B$, the space of all pure functions mapping $A$ to $B$.

The next natural choice of type constructor is derived from the existence of linear combinations of terms. First, $\flat{A}$ is the basis of $A$, that is: the minimal set of basis vectors that generate all vectors of type $A$ by (weak) linear combinations. Note that in general, $\flat{A}$ is not a subtype of $A$. Then, $\sharp{A}$ is the unitary span of $A$, that is: the type of all unitary vectors that can be formed as a (weak) linear combination of vectors of type $A$. Note that $A$ is always a subtype of $\sharp{A}$.

The last non-trivial type is $A\Rightarrow B$: the space of all unitary function distributions mapping $A$ to $B$. As lambda-terms are not distributives over linear combinations, this type is distinct from $\sharp{(A\rightarrow B)}$ (see next remark for a discussion). However, by construction, $A\to B$ is always a subtype of $A\Rightarrow B$.

Finally, we provide some syntactic sugar: the type of Booleans, the direct sum and the tensor product are defined by $\mathbb{B}:=\mathbb{U}+\mathbb{U}$, $A\oplus B:=\sharp(A+B)$, and $A\otimes B:=\sharp(A\times B)$.

The type $\sharp\mathbb{B}=\sharp(\mathbb{U}+\mathbb{U})=\mathbb{U}\oplus\mathbb{U}$ will be called the type of unitary Booleans. Notice that its semantics is given by the definition $\llbracket\sharp\mathbb{B}\rrbracket=\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})\cap\mathcal{S}_{1}$, that is, the set \bigl{\{}\alpha\cdot\mathtt{t\!t}:|\alpha|=1\bigr{\}}\cup\bigl{\{}\beta\cdot\mathtt{f\!f}:|\beta|=1\bigr{\}}\cup\bigl{\{}\alpha\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f}:|\alpha|^{2}+|\beta|^{2}=1\bigr{\}}.

Remarks IV.6**.**

The type constructors $\flat$ and $\sharp$ are monotonic and idempotent: $\flat\flat{A}\simeq\flat{A}$ and $\sharp\sharp{A}\simeq\sharp{A}$. 2. 2.

We always have the inclusion $A\leq\sharp{A}$, but the inclusion $\flat{A}\leq A$ does not hold in general. For instance, given any type $A$, we easily check that \frac{3}{5}\cdot\bigl{(}\lambda x\,{.}\,\frac{5}{6}\cdot x\bigr{)}+\frac{4}{5}\cdot\bigl{(}\lambda x\,{.}\,\frac{5}{8}\cdot x\bigr{)}~{}\in~{}\llbracket A\Rightarrow A\rrbracket\,, so that $(\lambda x\,{.}\,\frac{5}{6}\cdot x),(\lambda x\,{.}\,\frac{5}{8}\cdot x)\in\flat\llbracket A\Rightarrow A\rrbracket=\llbracket\flat(A\Rightarrow A)\rrbracket$. On the other hand, it is also clear that $(\lambda x\,{.}\,\frac{5}{6}\cdot x),(\lambda x\,{.}\,\frac{5}{8}\cdot x)\notin\llbracket A\Rightarrow A\rrbracket$ (unless $\llbracket A\rrbracket=\varnothing$). Therefore, $\flat(A\Rightarrow A)\not\leq A\Rightarrow A$. 3. 3.

We have the equivalence $\flat\sharp{A}\simeq\flat{A}$, but only the inclusion $A\leq\sharp\flat{A}$. More generally, the type constructor $\flat$ commutes with $+$ and $\times$: $\flat(A+B)\simeq\flat{A}+\flat{B}$ and $\flat(A\times B)\simeq\flat{A}\times\flat{B}$ but the type constructor $\sharp$ does not, since we only have the inclusions $\sharp{A}+\sharp{B}\leq\sharp(A+B)$ and $\sharp{A}\times\sharp{B}\leq\sharp(A\times B)$ 4. 4.

The inclusions  $A\Rightarrow B\leq\sharp(A\Rightarrow B)$  and  $\sharp(A\rightarrow B)\leq\sharp(A\Rightarrow B)$  are strict in general (unless the type $A\Rightarrow B$ is empty). As a matter of fact, the two types $\sharp(A\rightarrow B)$ and $\sharp(A\Rightarrow B)$ have no interesting properties—for instance, they are not subtypes of $\sharp{A}\Rightarrow\sharp{B}$. In practice, the type constructor $\sharp$ is only used on top of an algebraic type, constructed using one of $\mathbb{U}$, $+$, or $\times$.

IV-D1 Pure types and simple types

In what follows, we shall say that a type $A$ is pure when its unitary semantics only contains pure values, that is: when $\llbracket A\rrbracket\subseteq\mathrm{V}$. Equivalently, a type $A$ is pure when the type equivalence $\flat{A}\simeq A$ is valid (or when $A\leq\flat{B}$ for some type $B$). We easily check that:

Lemma IV.7**.**

For all types $A$ and $B$:

The types $\mathbb{U}$, $\flat{A}$ and $A\rightarrow B$ are pure. 2. 2.

If $A$ and $B$ are pure, then so are $A+B$ and $A\times B$. 3. 3.

$\sharp{A}$* and $A\Rightarrow B$ are not pure, unless they are empty. ∎*

A particular case of pure types are the simple types, that are syntactically defined from the following sub-grammar of the grammar of Table IV:

[TABLE]

It is clear from Lemma IV.7 that all simple types are pure types. The converse is false, since the type $\sharp\mathbb{U}\rightarrow\sharp\mathbb{U}$ is pure, although it is not generated from the above grammar.

IV-D2 Pure arrow vs unitary arrow

The pure arrow $A\rightarrow B$ and the unitary arrow $A\Rightarrow B$ only differ in the shape of the functions which they contain: the pure arrow $A\rightarrow B$ only contains pure abstractions whereas the unitary arrow $A\Rightarrow B$ contains arbitrary unitary distributions of abstractions mapping values of type $A$ to realizers of type $B$. However, the functions that are captured by both sets $\llbracket A\rightarrow B\rrbracket\subseteq\mathrm{V}$ and $\llbracket A\Rightarrow B\rrbracket\subseteq\mathcal{S}_{1}$ are extensionally the same:

Proposition IV.8**.**

For all unitary distributions of abstractions \bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1}, one has:

[TABLE]

IV-E Representation of unitary operators

Recall that the type of unitary Booleans is defined as $\sharp\mathbb{B}=\sharp(\mathbb{U}+\mathbb{U})=\mathbb{U}\oplus\mathbb{U}$, so that for all closed term distributions $\vec{t}$, we have $\vec{t}\Vdash\sharp\mathbb{B}$ iff

[TABLE]

We can observe that the unitary semantics of the type $\sharp\mathbb{B}$ simultaneously contains the vectors $\alpha\cdot\mathtt{t\!t}$ and $\alpha\cdot\mathtt{t\!t}+0\cdot\mathtt{f\!f}$, that can be considered as “morally” equivalent (although they are not according to the congruence $\equiv$). To identify such vectors, it is convenient to introduce the Boolean projection $\pi_{\mathbb{B}}:\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})\to\mathbb{C}^{2}$ defined by

[TABLE]

for all $\alpha,\beta\in\mathbb{C}$. By construction, the function $\pi_{\mathbb{B}}:\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})\to\mathbb{C}^{2}$ is linear, surjective, and neglects the difference between $\alpha\cdot\mathtt{t\!t}+0\cdot\mathtt{f\!f}$ and $\alpha\cdot\mathtt{t\!t}$ (and between $0\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f}$ and $\beta\cdot\mathtt{f\!f}$). Moreover, the map $\pi_{\mathbb{B}}:\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})\to\mathbb{C}^{2}$ preserves the inner product, in the sense that for all $\vec{v},\vec{w}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$, we have

[TABLE]

Definition IV.9**.**

We say that a closed term distribution $\vec{t}$ represents a function $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$ when for all $\vec{v}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$, there exists $\vec{w}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ such that

[TABLE]

Remark IV.10**.**

From the bilinearity of application, it is clear that each function $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$ that is represented by a closed term distribution is necessarily linear.

Recall that an operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$ is unitary when it preserves the inner product of $\mathbb{C}^{2}$, in the sense that $\langle{F(u)}~{}|~{}{F(v)}\rangle=\langle{u}~{}|~{}{v}\rangle$ for all $u,v\in\mathbb{C}^{2}$. Equivalently, an operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$ is unitary if and only if $\|F(1,0)\|_{\mathbb{C}^{2}}=\|F(0,1)\|_{\mathbb{C}^{2}}=1$ and $\langle{F(1,0)}~{}|~{}{F(0,1)}\rangle_{\mathbb{C}^{2}}=0$. The following propositions expresses that the types $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ and $\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$ capture unitary operators:

Proposition IV.11**.**

Given a closed $\lambda$-abstraction $\lambda x\,{.}\,\vec{t}$, we have $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$ if and only if there are two value distributions $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$ such that we have $\vec{t}\,[x:=\mathtt{t\!t}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$, $\vec{t}\,[x:=\mathtt{f\!f}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$ and $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$.∎

Theorem IV.12** **(Characterization of the values of type

$\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$).

A closed $\lambda$-abstraction $\lambda x\,{.}\,\vec{t}$ is a value of type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ if and only if it represents a unitary operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$.∎

Corollary IV.13** **(Characterization of the values of type

$\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$).

A unitary distribution of abstractions \bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1} is a value of type $\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$ if and only if it represents a unitary operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$.∎

V Typing Judgements

In Section IV, we introduced a simple type algebra (Table IV) together with the corresponding unitary semantics (Table V). We also introduced the two judgments $A\leq B$ and $A\simeq B$. Now, it is time to introduce the typing judgment $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A$ together with the corresponding notion of validity.

V-A Typing Rules

As usual, we call a typing context (or a context) any finite function from the set of variables to the set of types. Contexts $\Gamma$ are traditionally written $\Gamma~{}=~{}x_{1}:A_{1},\ldots,x_{\ell}:A_{\ell}$ where $\{x_{1},\ldots,x_{\ell}\}=\mathrm{dom}(\Gamma)$ and where $A_{i}=\Gamma(x_{i})$ for all $i=1..\ell$. The empty context is written $\emptyset$, and the concatenation of two contexts $\Gamma$ and $\Delta$ such that $\mathrm{dom}(\Gamma)\cap\mathrm{dom}(\Delta)=\varnothing$ is defined by $\Gamma,\Delta:=\Gamma\cup\Delta$ (that is: as the union of the underlying functions).

Similarly, we call a substitution any finite function from the set of variables to the set $\vec{\mathrm{V}}$ of closed value distributions. Substitutions $\sigma$ are traditionally written $\sigma~{}=~{}\{x_{1}:=\vec{v}_{1},\ldots,x_{\ell}:=\vec{v}_{\ell}\}$ where $\{x_{1},\ldots,x_{\ell}\}=\mathrm{dom}(\sigma)$ and where $\vec{v}_{i}=\sigma(x_{i})$ for all $i=1..\ell$. The empty substitution is written $\emptyset$, and the concatenation of two substitutions $\sigma$ and $\tau$ such that $\mathrm{dom}(\sigma)\cap\mathrm{dom}(\tau)=\varnothing$ is defined by $\sigma,\tau:=\sigma\cup\tau$ (that is: as the union of the underlying functions). Given an open term distribution $\vec{t}$ and a substitution $\sigma=\{x_{1}:=\vec{v}_{1},\ldots,x_{\ell}:=\vec{v}_{\ell}\}$, we write $\vec{t}\,\langle\sigma\rangle~{}:=~{}\vec{t}\,\langle x_{1}:=\vec{v}_{1}\rangle\cdots\langle x_{\ell}:=\vec{v}_{\ell}\rangle\,.$ Note that since the value distributions $\vec{v}_{1},\ldots,\vec{v}_{\ell}$ are closed, the order in which the (closed) bilinear substitutions $\langle x_{i}:=\vec{v}_{i}\rangle$ ($i=1..\ell$) are applied to $\vec{t}$ is irrelevant.

Definition V.1** **(Unitary semantics of a typing

context).

Given a typing context $\Gamma$, we call the unitary semantics of $\Gamma$ and write $\llbracket\Gamma\rrbracket$ the set of substitutions defined by

[TABLE]

Finally, we call the strict domain of a context $\Gamma$ and write $\mathrm{dom}^{\sharp}(\Gamma)$ the set

[TABLE]

Intuitively, the elements of the set $\mathrm{dom}^{\sharp}(\Gamma)$ are the variables of the context $\Gamma$ whose type is not a type of pure values. As we shall see below, these variables are the variables that must occur in all the term distributions that are well-typed in the context $\Gamma$. (This restriction is essential to ensure the validity of the rule (UnitLam), Table VI).

Definition V.2** (Typing judgments).**

A typing judgment is a triple $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A$ formed by a typing context $\Gamma$, a (possibly open) term distribution $\vec{t}$ and a type $A$. This judgment is valid when:

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$; and 2. 2.

$\vec{t}\langle\sigma\rangle\Vdash A$* for all $\sigma\in\llbracket\Gamma\rrbracket$.*

Proposition V.3**.**

The typing rules of Table VI are valid.∎

Remark V.4**.**

In the rule (PureLam), the notation $\flat{\Gamma}\simeq\Gamma$ refers to the conjunction of premises $\flat{A_{1}}\simeq A_{1}~{}\&~{}\cdots~{}\&~{}\flat{A_{\ell}}\simeq A_{\ell}$, where $A_{1},\ldots,A_{\ell}$ are the types occurring in the context $\Gamma$.

Remark V.5**.**

The proof of validity of the typing rule (UnitLam) crucially relies on the fact that the body $\vec{t}$ of the abstraction $\lambda x\,{.}\,\vec{t}$ is a raw distribution (i.e. an expression that is considered only up to $\alpha$-conversion, and not $\equiv$). This is the reason why we endowed term distributions (Section II-B) with the congruence $\equiv$ that is shallow, in the sense that it does not propagate in the bodies of abstractions, in the bodies of let-constructs, or in the branches of match-constructs.

V-B Simply-typed lambda-calculus

Recall that simple types (Section IV-D1) are generated from the following sub-grammar of the grammar of Table IV:

[TABLE]

By construction, all simple types $A$ are pure types, in the sense that $\flat{A}\simeq A$. Since pure types allow the use of weakening and contraction, it is a straightforward exercise to check that any typing judgment  $\Gamma~{}{\vdash}~{}t~{}{:}~{}A$  that is derivable in the simply-typed $\lambda$-calculus with sums and products is also derivable from the typing rules of Table VI.

V-C Typing Church numerals

Let us recall that Church numerals $\bar{n}$ are defined for all $n\in\mathbb{N}$ by $\bar{n}~{}:=~{}\lambda f\,{.}\,\lambda x\,{.}\,f^{n}\,x$. From the typing rules of Table VI, we easily derive that $~{}{\vdash}~{}\bar{n}~{}~{}{:}~{}~{}(\mathbb{B}\rightarrow\mathbb{B})\rightarrow(\mathbb{B}\rightarrow\mathbb{B})$ (by simple typing) and even that $~{}{\vdash}~{}\bar{n}~{}~{}{:}~{}~{}(\sharp\mathbb{B}\rightarrow\sharp\mathbb{B})\rightarrow(\sharp\mathbb{B}\rightarrow\sharp\mathbb{B})$, using the fact that $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ is a pure type, that is subject to arbitrary weakenings and contractions. On the other hand, since we cannot use weakening or contraction for the non pure type $\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$, we cannot derive the judgments $~{}{\vdash}~{}\bar{n}~{}~{}{:}~{}~{}(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})\rightarrow(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})$ and $~{}{\vdash}~{}\bar{n}~{}~{}{:}~{}~{}(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})\Rightarrow(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})$ but for $n=1$. (cf. Fact .11 in Appendix -C).

V-D Orthogonality as a Typing Rule

The typing rules of Table VI allow us to derive that the terms $I:=\lambda x\,{.}\,x$, $K_{\mathtt{t\!t}}:=\lambda x\,{.}\,\mathtt{t\!t}$, $K_{\mathtt{f\!f}}:=\lambda x\,{.}\,\mathtt{f\!f}$ and $N:=\lambda x\,{.}\,\mathtt{i{\mskip-1.0mu}f}~{}x~{}\{\mathtt{f\!f}\mid\mathtt{t\!t}\}$ have type $\mathbb{B}\rightarrow\mathbb{B}$; they even allow us to derive that $I$ has type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$, but they do not allow us (yet) to derive that the Boolean negation $N$ or the Hadamard $H$ have type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$. For that, we need to introduce a new form of judgment: orthogonality judgments.

Definition V.6** (Orthogonality judgments).**

An orthogonality judgment is a sextuple

[TABLE]

formed by three typing contexts $\Gamma$, $\Delta_{1}$ and $\Delta_{2}$, two (possibly open) term distributions $\vec{t}_{1}$, $\vec{t}_{2}$ and a type $A$. This judgment is valid when:

both judgments $\Gamma,\Delta_{1}~{}{\vdash}~{}\vec{t}_{1}~{}{:}~{}A$ and $\Gamma,\Delta_{2}~{}{\vdash}~{}\vec{t}_{2}~{}{:}~{}A$ are valid; and 2. 2.

for all $\sigma\in\llbracket\Gamma\rrbracket$, $\sigma_{1}\in\llbracket\Delta_{1}\rrbracket$ and $\sigma_{2}\in\llbracket\Delta_{2}\rrbracket$, if $\vec{t}_{1}\langle\sigma,\sigma_{1}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$ and $\vec{t}_{2}\langle\sigma,\sigma_{2}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$,

then $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$.

When both contexts $\Delta_{1}$ and $\Delta_{2}$ are empty, the orthogonality judgment $\Gamma~{}{\vdash}~{}(\Delta_{1}~{}{\vdash}~{}\vec{t}_{1})\perp(\Delta_{2}~{}{\vdash}~{}\vec{t}_{2})~{}{:}~{}A$ is simply written $\Gamma~{}{\vdash}~{}\vec{t}_{1}\perp\vec{t}_{2}~{}{:}~{}A$.

With this definition, we can prove a new typing rule, which can be used to type Hadamard:

Proposition V.7**.**

The rule (UnitaryMatch) given below is valid.

$\Gamma,\Delta~{}{\vdash}~{}\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}~{}{:}~{}\sharp C\lx@proof@logical@and\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A_{1}\oplus A_{2}\Delta~{}{\vdash}~{}(x_{1}:\sharp A_{1}~{}{\vdash}~{}\vec{s}_{1})\perp(x_{2}:\sharp A_{2}~{}{\vdash}~{}\vec{s}_{2})~{}{:}~{}\sharp C$

∎

Example V.8**.**

We have $~{}{\vdash}~{}\mathtt{t\!t}\perp\mathtt{f\!f}~{}{:}~{}\mathbb{B}$. Consider the terms $|+\rangle=\frac{1}{\sqrt{2}}\cdot\mathtt{t\!t}+\frac{1}{\sqrt{2}}\cdot\mathtt{f\!f}$ and $|-\rangle=\frac{1}{\sqrt{2}}\cdot\mathtt{t\!t}+(-\frac{1}{\sqrt{2}})\cdot\mathtt{f\!f}$. Then we can prove that $~{}{\vdash}~{}|+\rangle\perp|-\rangle~{}{:}~{}\sharp\mathbb{B}.$

We can also prove that

[TABLE]

Using this fact, and the rule (UnitaryMatch) from Proposition V.7, we can derive the type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ for the Hadamard gate $H$ defined in Example III.6. Recall that $\sharp\mathbb{B}=\sharp(\mathbb{U}+\mathbb{U})=\mathbb{U}\oplus\mathbb{U}$.

VI Unifying Model of Classical and Quantum Control

We showed in Section V-B that the unitary linear algebraic lambda calculus strictly contains the simply-typed lambda calculus. With Theorem IV.12 and Corollary IV.13 we expressed how the “only” valid functions were unitary maps, and in Section V-D we hinted at how to type orthogonality with the model. This section is devoted to showing how the model can be used as a model for quantum computation, with the model providing an operational semantics to a high-level operation on circuits: the control of a circuit.

VI-A A Quantum Lambda-Calculus

The language we consider, called $\lambda_{Q}$, is a circuit-description language similar to QWIRE [6] or Proto-Quipper [26]. Formally, the types of $\lambda_{Q}$ are defined from the following grammar:

[TABLE]

The types denoted by $A$, $B$ are the usual simple types, which we call classical types. (Note that they contain a type $\mathsf{bit}$ of classical bits, that corresponds to the type $\mathbb{U}+\mathbb{U}$ in our model.) The types denoted by $A_{Q}$, $B_{Q}$ are the quantum types; they basically consist in tensor products of the type $\mathsf{qbit}$ of quantum bits. As the former types are duplicable while the latter are non-duplicable, we define a special (classical) function-type $A_{Q}\multimap B_{Q}$ between quantum types.

The term syntax for $\lambda_{Q}$ is defined from the following grammar:

[TABLE]

The first two lines of the definition describe the usual constructions of the simply-typed lambda calculus with (ordinary) pairs. The last two lines adds the quantum specificities: a tensor for dealing with systems of several quantum bits (together with the corresponding destructor), an operator $\mathsf{new}$ to create a new quantum bit, and a family of operators $U(t)$ to apply a given unitary operator on $t$. We also provide a special lambda abstraction $\lambda^{Q}$ to make a closure out of a quantum computation, as well as a special application to apply such a closure. Note that for simplicity, we only consider unary quantum operators—that is: operators on the type $\mathsf{qbit}$—, but this can be easily extended to quantum operators acting on tensor products of the form $\mathsf{qbit}^{{\otimes}n}$. Also note that we do not consider measurements, for our realizability model does not natively support it.

The language $\lambda_{Q}$ features two kinds of typing judgments: a classical judgment $\Delta\vdash_{C}t:A$, where $\Delta$ is a typing context of classical types and where $A$ is a classical type, and a quantum judgment $\Delta|\Gamma\vdash_{Q}t:A_{Q}$, where $\Delta$ is a typing context of classical types, $\Gamma$ a typing context of quantum types, and where $A_{Q}$ is a quantum type. An empty typing context is always denoted by $\emptyset$. As usual, we write $\Gamma,\Delta$ for $\Gamma\cup\Delta$ (when $\Gamma\cap\Delta=\emptyset$), and we use the notation $\textit{FV}(t):\mathsf{qbit}$ to represent the quantum context $x_{1}:\mathsf{qbit},\ldots,x_{n}:\mathsf{qbit}$ made up of the finite set $\textit{FV}(t)=\{x_{1},\ldots,x_{n}\}$.

The typing rules for classical judgements are standard and are given in the Appendix -D. Rules for quantum judgements are given in the Table VII. The last three rules allows to navigate between classical and quantum judgments.

Note that in the above rules, classical variables (declared in the $\Delta$’s) can be freely duplicated whereas quantum variables (declared in the $\Gamma$’s) cannot. Also note that in $\lambda_{Q}$, pure quantum computations are essentially first-order.

The first of the last three rules makes a qbit out of a bit, the second rule makes a closure out of a quantum computation, while the third rule opens a closure containing a quantum computation. These last two operations give a hint of higher-order to quantum computations in $\lambda_{Q}$.

A value is a term belonging to the grammar:

[TABLE]

The language $\lambda_{Q}$ is equipped with the standard operational semantics presented in [27]: the quantum environment is separated from the term, in the spirit of the QRAM model of [4]. Formally, a program is defined as a triplet $[Q,L,t]$ where $t$ is a term, $L$ is a bijection from $FV(t)$ to $\{1,\dots,n\}$ and $Q$ is an $n$-quantum bit system: a normalized vector in the $2^{n}$-dimensional vector space $(\mathbb{C}^{2})^{\otimes n}$. We say that a program $[Q,L,t]$ is well-typed of type $A_{Q}$ when the judgment $\emptyset|\textit{FV}(t):\mathsf{qbit}\vdash_{Q}t:A_{Q}$ is derivable. In particular, well-typed programs correspond to quantum typing judgements, closed with respect to classically-typed term-variables.

The operational semantics is call-by-value and relies on applicative contexts, that are defined as follows:

[TABLE]

The operational semantics of the calculus is formally defined from the rules given in Table VIII.

The language $\lambda_{Q}$ satisfies the usual safety properties, proved as in [27].

Theorem VI.1** (Safety properties).**

If $[Q,L,t]:A_{Q}$ and $[Q,L,t]\to[Q^{\prime},L^{\prime},r]$, then $[Q^{\prime},L^{\prime},r]:A_{Q}$. Moreover, whenever a program $[Q,L,t]$ is well-typed, either $t$ is already a value or it reduces to some other program. ∎

VI-B Modelling $\lambda_{Q}$

The realizability model based on the unitary linear-algebraic lambda-calculus is a model for the quantum lambda-calculus $\lambda_{Q}$. We write $\llparenthesis{t}\rrparenthesis$ for the translation of a term of $\lambda_{Q}$ into its model. The model can indeed not only accomodate classical features, using pure terms, but also quantum states, using linear combinations of terms.

We map $\mathsf{qbit}$ to $\sharp\mathbb{B}$ and $\mathsf{bit}$ to $\mathbb{B}$. This makes $\mathsf{bit}$ a subtype of $\mathsf{qbit}$: the model captures the intuition that booleans are “pure” quantum bits. Classical arrows $\to$ are mapped to $\to$ and classical product $\times$ is mapped to the product of the model, in the spirit of the encoding of simply-typed lambda-calculus. Finally, the tensor of $\lambda_{Q}$ is mapped to the tensor of the model.

The interesting type is $A_{Q}\multimap B_{Q}$. We need this type to be both classical and capture the fact that a term of this type is a pure quantum computation from $A_{Q}$ to $B_{Q}$, that is, a unitary map. The encoding we propose consists in using “thunk”, as proposed by [28]. Formally, the translation of types is as follows: $\llparenthesis{\mathsf{bit}}\rrparenthesis=\mathbb{B}$, $\llparenthesis{A\times B}\rrparenthesis=\llparenthesis{A}\rrparenthesis\times\llparenthesis{B}\rrparenthesis$, $\llparenthesis{A\to B}\rrparenthesis=\llparenthesis{A}\rrparenthesis\to\llparenthesis{B}\rrparenthesis$, $\llparenthesis{A_{Q}\multimap B_{Q}}\rrparenthesis=\mathbb{U}\to(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis)$, $\llparenthesis{\mathsf{qbit}}\rrparenthesis=\sharp\mathbb{B}$, $\llparenthesis{A_{Q}\otimes B_{Q}}\rrparenthesis=\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis=\sharp(\llparenthesis{A_{Q}}\rrparenthesis\times\llparenthesis{B_{Q}}\rrparenthesis)$, and $\llparenthesis{\mathbb{U}}\rrparenthesis=\mathbb{U}$.

Lemma VI.2**.**

For all classical types $A$, $\flat\llparenthesis{A}\rrparenthesis\simeq\llparenthesis{A}\rrparenthesis$.∎

Lemma VI.3**.**

For all qbit types $A_{Q}$, $\sharp\llparenthesis{A_{Q}}\rrparenthesis\simeq\llparenthesis{A_{Q}}\rrparenthesis$.∎

The classical structural term constructs of $\lambda_{Q}$ are translated literally: $\llparenthesis{x}\rrparenthesis=x$, $\llparenthesis{*}\rrparenthesis=*$, $\llparenthesis{\lambda x.t}\rrparenthesis=\lambda x.\llparenthesis{t}\rrparenthesis$, $\llparenthesis{tr}\rrparenthesis=\llparenthesis{t}\rrparenthesis\llparenthesis{r}\rrparenthesis$, $\llparenthesis{(t,r)}\rrparenthesis=(\llparenthesis{t}\rrparenthesis,\llparenthesis{r}\rrparenthesis)$, $\llparenthesis{\mathtt{i{\mskip-1.0mu}f}~{}t~{}\{r\mid s\}}\rrparenthesis=\texttt{match}~{}\llparenthesis{t}\rrparenthesis~{}\{\texttt{inl}(z_{1})\mapsto z_{1};{\llparenthesis{r}\rrparenthesis}~{}|~{}\texttt{inr}(z_{2})\mapsto z_{2};{\llparenthesis{s}\rrparenthesis}\}$ with $z_{1}$ and $z_{2}$ fresh variables, $\llparenthesis{\mathtt{t\!t}}\rrparenthesis=\texttt{inl}(*)$, $\llparenthesis{\mathtt{f\!f}}\rrparenthesis=\texttt{inr}(*)$, $\llparenthesis{\pi_{i}(t)}\rrparenthesis=\mathsf{let}\ {(x_{1},x_{2})}={\llparenthesis{t}\rrparenthesis}\ \mathsf{in}\ {x_{i}}$. Finally, the term constructs related to quantum bits make use of the algebraic aspect of the language. First, $\mathsf{new}$ is simply the identity, since booleans are subtypes of quantum bits: $\llparenthesis{\mathsf{new}(t)}\rrparenthesis=\llparenthesis{t}\rrparenthesis$. Then, the translation of the unitary operators is done with the construction already encountered in e.g. Example III.6: $\llparenthesis{U(t)}\rrparenthesis=\bar{U}\llparenthesis{t}\rrparenthesis$ where $\bar{U}$ is defined as follows. If $U=(\begin{smallmatrix}a&b\\ c&d\end{smallmatrix})$, then $\bar{U}=\lambda x.\texttt{match}~{}x~{}\{\texttt{inl}(x_{1})\mapsto a\cdot\texttt{inl}(x_{1})+c\cdot\texttt{inr}(x_{1})~{}|~{}\texttt{inr}(x_{2})\mapsto b\cdot\texttt{inl}(x_{2})+d\cdot\texttt{inr}(x_{2})\}$.

Then, the tensor is defined with the pairing construct, which is distributive: $\llparenthesis{t\otimes r}\rrparenthesis=(\llparenthesis{t}\rrparenthesis,\llparenthesis{r}\rrparenthesis)$ and $\llparenthesis{\mathsf{let}\ {x\otimes y}={s}\ \mathsf{in}\ {t}}\rrparenthesis=\mathsf{let}\ {(x,y)}={\llparenthesis{s}\rrparenthesis}\ \mathsf{in}\ {\llparenthesis{t}\rrparenthesis}$. Finally, the quantum closure and applications are defined by remembering the use of the thunk: $\llparenthesis{\lambda^{Q}x.t}\rrparenthesis=\lambda zx.\llparenthesis{t}\rrparenthesis$, where $z$ is a fresh variable, and $\llparenthesis{t\MVAt r}\rrparenthesis=(\llparenthesis{t}\rrparenthesis*)\llparenthesis{r}\rrparenthesis$: one first “open” the thunk before applying the function.

We also define the translation of typing contexts as follows: if $\Gamma=\{x_{i}:A_{i}\}_{i}$, we write $\llparenthesis{\Gamma}\rrparenthesis$ for $\{x_{i}:\llparenthesis{A_{i}}\rrparenthesis\}_{i}$, and we write $\llparenthesis{\Delta|\Gamma}\rrparenthesis$ for $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis$. Finally, a program is translated as follows: $\llparenthesis{[\sum_{i=1}^{m}\alpha_{i}.|y_{1}^{i},\dots,y_{n}^{i}\rangle,\{x_{1}:=p(1),\dots,x_{n}:=p(n)\},t]}\rrparenthesis=\sum_{i=1}^{m}\alpha_{i}\cdot\llparenthesis{t}\rrparenthesis[x_{1}:=\bar{y}_{p(1)}^{i},\dots,x_{n}:=\bar{y}_{p(n)}^{i}]$ where $p$ is a permutation of $n$ and $\bar{0}=\mathtt{t\!t}$ and $\bar{1}=\mathtt{f\!f}$.

Example VI.4**.**

Let $P$ be the program $[\alpha|00\rangle+\beta|11\rangle,\{x:=1,y:=2\},(x\otimes y)]$. It consists on a pair of the two quantum bits given in the quantum context on the first component of the triple. The translation of this program is as follows. $\llparenthesis{P}\rrparenthesis\ =\ \alpha\cdot(x,y)[x:=\mathtt{t\!t},y:=\mathtt{t\!t}]+\beta\cdot(x,y)[x:=\mathtt{f\!f},y:=\mathtt{f\!f}]\ =\ \alpha\cdot(\mathtt{t\!t},\mathtt{t\!t})+\beta\cdot(\mathtt{f\!f},\mathtt{f\!f})$.

The translation is compatible with typing and rewriting. This is to be put in reflection with Theorem IV.12: not only the realizability model captures unitarity, but it is expressive enough to comprehend a higher-order quantum programming language.

Theorem VI.5**.**

Translation preserves typeability:

If $\Gamma\vdash_{Q}t:A_{Q}$ then $\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis$. 2. 2.

If $\Delta|\Gamma\vdash_{C}t:A$ then $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis$. 3. 3.

If $[Q,L,t]:A$ then $\vdash\llparenthesis{[Q,L,t]}\rrparenthesis:\llparenthesis{A}\rrparenthesis$.∎

Theorem VI.6** (Adequacy).**

If $[Q,L,t]\to[Q^{\prime},L^{\prime},r]$, then $\llparenthesis{[Q,L,t]}\rrparenthesis\mathrel{{\succ}\mskip-6.0mu{\succ}}\llparenthesis{[Q^{\prime},L^{\prime},r]}\rrparenthesis$. ∎

VI-C A Circuit-Description Language

Quantum algorithms do not only manipulate quantum bits: they also manipulate circuits. A quantum circuit is a sequence of elementary operations that are buffered before being sent to the quantum memory. If one can construct a quantum circuit by concatenating elementary operations, several high-level operations on circuits are allowed for describing quantum algorithms: repetition, control (discussed in Section VI-D), inversion, etc.

In recent years, several quantum programming languages have been designed to allow the manipulation of circuits: Quipper [5] and its variant ProtoQuipper [26], QWIRE [6], etc. These languages share a special function-type $\mathsf{Circ}(A,B)$ standing for the type of circuits from wires of type $A$ to wires of type $B$. Two built-in constructors are used to go back and forth between circuits and functions acting on quantum bits:

• •

$\mathsf{box}:(A_{Q}\,{\multimap}\,B_{Q})\to\mathsf{Circ}(A_{Q},B_{Q})$. Its operational semantics is to evaluate the input function on a phantom element of type $A$, collect the list of elementary quantum operations to be performed and store them in the output circuit.

• •

$\mathsf{unbox}:\mathsf{Circ}(A_{Q},B_{Q})\to(A_{Q}\multimap B_{Q})$. This operator is the dual: it takes a circuit — a list of elementary operations — and return a concrete function.

The advantage of distinguishing between functions and circuits is that a circuit is a concrete object: it is literally a list of operations that can be acted upon. A function is a suspended computation: it is a priori not possible to inspect its body.

The language $\lambda_{Q}$ does not technically possess a type constructor for circuits: the typing construct $\multimap$ is really a lambda-abstraction. However, it is very close to being a circuit: one could easily add a typing construct $\mathsf{Circ}$ in the classical type fragment and implement operators $\mathsf{box}$ and $\mathsf{unbox}$, taking inspiration for the operational semantics on what has been done by [26] for ProtoQuipper.

How would this be reflected in the realizability model? We claim that the translation of the type $\mathsf{Circ}(A_{Q},B_{Q})$ can be taken to be the same as the translation of $A_{Q}\multimap B_{Q}$, the operator $\mathsf{box}$ and $\mathsf{unbox}$ simply being the identity. The realizability model is then rich enough to express several high-level operations on circuits: this permits to extend the language $\lambda_{Q}$. The fact that the model “preserves unitarity” (Theorem IV.12) ensuring the soundness of the added constructions.

In what follows, by abuse of notation, we identify $\mathsf{Circ}(A_{Q},B_{Q})$ and $A_{Q}\multimap B_{Q}$.

VI-D Control Operator

Suppose that we are given a closed term $t$ of $\lambda_{Q}$ with type $\mathsf{qbit}\multimap\mathsf{qbit}$. This function corresponds to a unitary matrix $U=(\begin{smallmatrix}a&b\\ c&d\end{smallmatrix})$, sending $|0\rangle$ to $a|0\rangle+c|1\rangle$ and $|1\rangle$ to $b|0\rangle+d|1\rangle$. We might want to write $\mathsf{ctl}(t)$ of type $(\mathsf{qbit}\otimes\mathsf{qbit})\multimap(\mathsf{qbit}\otimes\mathsf{qbit})$ behaving as the control of U, whose behavior is to send $|0\rangle\otimes\phi$ to $|0\rangle\otimes\phi$ and $|1\rangle\otimes\phi$ to $|1\rangle\otimes(U\phi)$: if the first input quantum bit is in state $|0\rangle$, control-U acts as the identity. If the first input quantum bit is in state $|1\rangle$, control-U performs U on the second quantum bit.

This is really a “quantum test” [29]. It has been formalized in the context of linear algebraic lambda-calculi by [1]. It can be ported to the unitary linear algebraic lambda-calculus as follows:

[TABLE]

and $\overline{\mathsf{ctl}}$ can be given the type

[TABLE]

Note how the definition is very semantical: the control operation is literally defined as a test on the first quantum bit.

We can then add an opaque term construct $\mathsf{ctl}(s)$ to $\lambda_{Q}$ with typing rule

[TABLE]

The translation of this new term construct is then $\llparenthesis{\mathsf{ctl}(t)}\rrparenthesis=\lambda z.(\overline{\mathsf{ctl}}({\llparenthesis{t}\rrparenthesis}*))$ with $z$ a fresh variable, and Theorem VI.6 still holds.

VII Conclusions

In this paper we have presented a language based on Lineal [1, 2]. Then, we have given a set of unitary types and proposed a realizability semantics associating terms and types.

The main result of this paper can be pinpointed to Theorem IV.12 and Corollary IV.13, which, together with normalization, progress, and subject reduction of the calculus (which are axiomatic properties in realizability models), imply that every term of type $\sharp B\rightarrow\sharp B$ represent a unitary operator. In addition, the Definition V.6 of orthogonal judgements led to Proposition V.7 proving rule (UnitaryMatch). Indeed, one of the main historic drawbacks for considering a calculus with quantum control has been to define the notion of orthogonality needed to encode unitary gates (cf., for example, [29]).

Finally, as an example to show the expressiveness of the language, we have introduced $\lambda_{Q}$ and showed that the calculus presented in this paper can be considered as a denotational semantics of it.

-A Proofs related to Section III

Lemma .1** (Simplifying equalities).**

Let scalars $\alpha_{1},\alpha_{2}\in\mathbb{C}$, pure terms $t_{1}$, $t_{2}$ and term distributions $\vec{s}_{1}$, $\vec{s}_{2}$ such that $\alpha_{1}\cdot t_{1}+\vec{s}_{1}\equiv\alpha_{2}\cdot t_{2}+\vec{s}_{2}$.

If $t_{1}=t_{2}=t$ and $\alpha_{1}=\alpha_{2}$, then: $\vec{s}_{1}\equiv\vec{s}_{2}$ or $\vec{s}_{1}\equiv\vec{s}_{2}+0\cdot t$ or $\vec{s}_{2}\equiv\vec{s}_{1}+0\cdot t$. 2. 2.

If $t_{1}=t_{2}=t$ but $\alpha_{1}\neq\alpha_{2}$, then: $\vec{s}_{1}\equiv\vec{s}_{2}+(\alpha_{2}-\alpha_{1})\cdot t$ or $\vec{s}_{2}\equiv\vec{s}_{1}+(\alpha_{1}-\alpha_{2})\cdot t$. 3. 3.

If $t_{1}\neq t_{2}$, then: $\vec{s}_{1}\equiv\vec{s}_{3}+\alpha_{2}\cdot t_{2}$ and $\vec{s}_{2}\equiv\vec{s}_{3}+\alpha_{1}\cdot t_{1}$ for some distribution $\vec{s}_{3}$.

(All the above disjunctions are inclusive). ∎

Lemma III.2 (Weak diamond). * if $\vec{t}\succ\vec{t}^{\prime}_{1}$ and $\vec{t}\succ\vec{t}^{\prime}_{2}$, then one of the following holds: either $\vec{t}^{\prime}_{1}=\vec{t}^{\prime}_{2}$; either $\vec{t}^{\prime}_{1}\succ\vec{t}^{\prime}_{2}$ or $\vec{t}^{\prime}_{2}\succ\vec{t}^{\prime}_{1}$; either $\vec{t}^{\prime}_{1}\succ\vec{t^{\prime\prime}}$ and $\vec{t}^{\prime}_{2}\succ\vec{t^{\prime\prime}}$ for some $\vec{t^{\prime\prime}}$. *

Proof of Lemma III.2.

Since $\vec{t}\succ\vec{t}^{\prime}_{1}$ and $\vec{t}\succ\vec{t}^{\prime}_{2}$, there are decompositions

[TABLE]

We distinguish three cases:

• •

Case where $s_{1}=s_{2}=s$ and $\alpha_{1}=\alpha_{2}=\alpha$. In this case, we have $\vec{s^{\prime}}_{1}=\vec{s^{\prime}}_{2}=\vec{s^{\prime}}$ since atomic evaluation is deterministic. And by Lemma .1 (1), we deduce that:

• –

Either $\vec{r}_{1}=\vec{r}_{2}$, so that: $\vec{t}^{\prime}_{1}~{}=~{}\alpha\cdot\vec{s^{\prime}}+\vec{r}_{1}~{}=~{}\alpha\cdot\vec{s^{\prime}}+\vec{r}_{2}~{}=~{}\vec{t}^{\prime}_{2}$.

• –

Either $\vec{r}_{1}=\vec{r}_{2}+0\cdot s$, so that:

[TABLE]

• –

Either $\vec{r}_{2}=\vec{r}_{1}+0\cdot s$, so that:

[TABLE]

• •

Case where $s_{1}=s_{2}=s$, but $\alpha_{1}\neq\alpha_{2}$. In this case, we have $\vec{s^{\prime}}_{1}=\vec{s^{\prime}}_{2}=\vec{s^{\prime}}$ since atomic evaluation is deterministic. And by Lemma .1 (2), we deduce that:

• –

Either $\vec{r}_{1}=\vec{r}_{2}+(\alpha_{2}-\alpha_{1})\cdot s$, so that:

[TABLE]

• –

Either $\vec{r}_{2}=\vec{r}_{1}+(\alpha_{1}-\alpha_{2})\cdot s$, so that:

[TABLE]

• •

Case where $s_{1}\neq s_{2}$. In this case, we know by Lemma .1 (3) that $\vec{r}_{1}=\vec{r}_{3}+\alpha_{2}\cdot s_{2}$ and $\vec{r}_{2}=\vec{r}_{3}+\alpha_{1}\cdot s_{1}$ for some $\vec{r}_{3}$. Writing $\vec{t^{\prime\prime}}=\alpha_{1}\cdot\vec{s^{\prime}}_{1}+\alpha_{2}\cdot\vec{s^{\prime}}_{2}+\vec{r}_{3}$, we conclude that

[TABLE]

-B Proofs related to Section IV

Proposition .2**.**

For all value distributions $\vec{v}_{1},\vec{v}_{2},\vec{w}_{1},\vec{w}_{2}$, we have:

[TABLE]

Proof.

Let us write $\vec{v}_{1}=\sum_{i_{1}=1}^{n_{1}}\alpha_{1,i_{1}}\cdot{v_{1,i_{1}}}$, $\vec{v}_{2}=\sum_{i_{2}=1}^{n_{2}}\alpha_{2,i_{2}}\cdot{v_{2,i_{1}}}$, $\vec{w}_{1}=\sum_{j_{1}=1}^{m_{1}}\beta_{1,j_{1}}\cdot{w_{1,j_{1}}}$ and $\vec{w}_{2}=\sum_{j_{2}=1}^{m_{2}}\beta_{2,j_{2}}\cdot{w_{2,j_{1}}}$ (all in canonical form). Writing $\delta_{v,v^{\prime}}=1$ when $v=v^{\prime}$ and $\delta_{v,v^{\prime}}=0$ when $v\neq v^{\prime}$ (Kronecker symbol), we observe that:

[TABLE]

[TABLE]

[TABLE]

The other equalities are proved similarly. ∎

Lemma IV.3. For all types $A$, we have $\llbracket A\rrbracket=\{{\Vdash}~{}A\}\cap\vec{\mathrm{V}}$.

Proof.

The inclusion $\llbracket A\rrbracket\subseteq\{{\Vdash}~{}A\}\cap\vec{\mathrm{V}}$ is clear from the definition of $\{{\Vdash}~{}A\}$. Conversely, suppose that $\vec{v}\in\{{\Vdash}~{}A\}\cap\vec{\mathrm{V}}$. From the definition of the set $\{{\Vdash}~{}A\}$, we know that $\vec{v}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v^{\prime}}$ for some $\vec{v^{\prime}}\in\llbracket A\rrbracket$. But since $\vec{v}$ is a normal form, we deduce that $\vec{v}=\vec{v^{\prime}}\in\llbracket A\rrbracket$. ∎

Lemma IV.5. Given any two types $A$ and $B$:

$A\leq B$* is valid if and only if $\{{\Vdash}~{}A\}\subseteq\{{\Vdash}~{}B\}$.* 2. 2.

$A\simeq B$* is valid if and only if $\{{\Vdash}~{}A\}=\{{\Vdash}~{}B\}$.*

Proof.

The direct implications are obvious from the definition of $\{{\Vdash}~{}A\}$, and the converse implications immediately follow from Lemma IV.3. ∎

Proposition IV.11. * Given a closed $\lambda$-abstraction $\lambda x\,{.}\,\vec{t}$, we have $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$ if and only if there are two value distributions $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$ such that*

[TABLE]

Proof.

The condition is necessary. Suppose that $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$. Since $\mathtt{t\!t},\mathtt{f\!f}\in\llbracket\sharp\mathbb{B}\rrbracket$, there are $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$ such that $\vec{t}\,[x:=\mathtt{t\!t}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$ and $\vec{t}\,[x:=\mathtt{f\!f}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$. It remains to prove that $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$. For that, consider $\alpha,\beta\in\mathbb{C}$ such that $|\alpha|^{2}+|\beta|^{2}=1$. By linearity, we observe that

[TABLE]

But since $\alpha\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f}\in\llbracket\sharp\mathbb{B}\rrbracket$, we must have $\alpha\cdot\vec{v}_{1}+\beta\cdot\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$ too, and in particular $\|\alpha\cdot\vec{v}_{1}+\beta\cdot\vec{v}_{2}\|=1$. From this, we get

[TABLE]

and thus $\mathrm{Re}(\bar{\alpha}\beta\,\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle)=0$. Taking $\alpha=\beta={\textstyle\frac{1}{\sqrt{2}}}$, we deduce that $\mathrm{Re}(\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle)=0$. And taking $\alpha=i{\textstyle\frac{1}{\sqrt{2}}}$ and $\beta={\textstyle\frac{1}{\sqrt{2}}}$, we deduce that $\mathrm{Im}(\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle)=0$. Therefore: $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$.

The condition is sufficient. Suppose that there are $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$ such that $\vec{t}\,[x:=\mathtt{t\!t}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$, $\vec{t}\,[x:=\mathtt{f\!f}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$ and $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$. In particular, we have $\vec{v}_{1},\vec{v}_{2}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ and $\|\vec{v}_{1}\|=\|\vec{v}_{2}\|=1$. Now, given any $\vec{v}\in\llbracket\sharp\mathbb{B}\rrbracket$, we distinguish three cases:

• •

Either $\vec{v}=\alpha\cdot\mathtt{t\!t}$, where $|\alpha|=1$. In this case, we observe that

[TABLE]

since $\alpha\cdot\vec{v}_{1}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ and $\|\alpha\cdot\vec{v}_{1}\|=|\alpha|\,\|\vec{v}_{1}\|=1$.

• •

Either $\vec{v}=\beta\cdot\mathtt{f\!f}$, where $|\beta|=1$. In this case, we observe that

[TABLE]

since $\beta\cdot\vec{v}_{2}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ and $\|\beta\cdot\vec{v}_{2}\|=|\beta|\,\|\vec{v}_{2}\|=1$.

• •

Either $\vec{v}=\alpha\cdot\mathtt{t\!t}+\beta\cdot\mathtt{f\!f}$, where $|\alpha|^{2}+|\beta|^{2}=1$. In this case, we observe that

[TABLE]

since $\alpha\cdot\vec{v}_{1}+\beta\cdot\vec{v}_{2}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ and

[TABLE]

We have thus shown that $\vec{t}\,\langle x:=\vec{v}\rangle\Vdash\sharp\mathbb{B}$ for all $\vec{v}\in\llbracket\sharp\mathbb{B}\rrbracket$. Therefore $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$. ∎

Theorem IV.12 (Characterization of the values of type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$). * A closed $\lambda$-abstraction $\lambda x\,{.}\,\vec{t}$ is a value of type $\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}$ if and only if it represents a unitary operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$. *

Proof.

The condition is necessary. Suppose that $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$. From Prop. IV.11, there are $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp{\mathbb{B}}\rrbracket$ such that $\vec{t}\,[x:=\mathtt{t\!t}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$, $\vec{t}\,[x:=\mathtt{f\!f}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$ and $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$. Let $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$ be the operator defined by $F(1,0)=\pi_{\mathbb{B}}(\vec{v}_{1})$ and $F(0,1)=\pi_{\mathbb{B}}(\vec{v}_{2})$. From the properties of linearity of the calculus, it is clear that the abstraction $\lambda x\,{.}\,\vec{t}$ represents the operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$. Moreover, the operator $F$ is unitary since $\|\pi_{\mathbb{B}}(\vec{v}_{1})\|_{\mathbb{C}^{2}}=\|\pi_{\mathbb{B}}(\vec{v}_{2})\|_{\mathbb{C}^{2}}=1$ and $\langle{\pi_{\mathbb{B}}(\vec{v}_{1})}~{}|~{}{\pi_{\mathbb{B}}(\vec{v}_{2})}\rangle_{\mathbb{C}^{2}}=0$.

The condition is sufficient. Let us assume that the abstraction $\lambda x\,{.}\,\vec{t}$ represents a unitary operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$. From this, we deduce that:

• •

$(\lambda x\,{.}\,\vec{t}\,)\,\mathtt{t\!t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}$ for some $\vec{v}_{1}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ such that $\pi_{\mathbb{B}}(\vec{v}_{1})=F(\pi_{\mathbb{B}}(\mathtt{t\!t}))=F(1,0)$;

• •

$(\lambda x\,{.}\,\vec{t}\,)\,\mathtt{f\!f}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}$ for some $\vec{v}_{2}\in\mathrm{span}(\{\mathtt{t\!t},\mathtt{f\!f}\})$ such that $\pi_{\mathbb{B}}(\vec{v}_{2})=F(\pi_{\mathbb{B}}(\mathtt{f\!f}))=F(0,1)$.

Using the property of confluence, we deduce that

• •

$\vec{t}\,[x:=\mathtt{t\!t}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{1}\in\llbracket\sharp\mathbb{B}\rrbracket$, since $\|\vec{v}_{1}\|=\|F(1,0)\|_{\mathbb{C}^{2}}=1$;

• •

$\vec{t}\,[x:=\mathtt{f\!f}]\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{2}\in\llbracket\sharp\mathbb{B}\rrbracket$, since $\|\vec{v}_{2}\|=\|F(0,1)\|_{\mathbb{C}^{2}}=1$.

We deduce that $\lambda x\,{.}\,\vec{t}\in\llbracket\sharp\mathbb{B}\rightarrow\sharp\mathbb{B}\rrbracket$ by Prop. IV.11, since $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=\langle{F(1,0)}~{}|~{}{F(0,1)}\rangle_{\mathbb{C}^{2}}=0$. ∎

Corollary IV.13 (Characterization of the values of type $\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$). * A unitary distribution of abstractions \bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1} is a value of type $\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$ if and only if it represents a unitary operator $F:\mathbb{C}^{2}\to\mathbb{C}^{2}$. *

Proof.

Indeed, given \bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1}, we have

[TABLE]

since both functions $\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}$ and \lambda x\,{.}\,\bigl{(}\sum_{i=1}^{n}\alpha_{i}\cdot\vec{t}_{i}\,\bigr{)} are extensionally equivalent. ∎

Lemma .3**.**

For all term distributions $\vec{t}$, $\vec{t}^{\prime}$, $\vec{s}$, $\vec{s}_{1}$, $\vec{s}_{2}$ and for all value distributions $\vec{v}$ and $\vec{w}$:

$(\lambda x\,{.}\,\vec{t}\,)\,\vec{v}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\vec{t}\,\langle x:=\vec{v}\rangle$** 2. 2.

$\texttt{let}~{}(x,y)=(\vec{v},\vec{w})~{}\texttt{in}~{}\vec{s}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\vec{s}\langle x:=\vec{v}\rangle\langle y:=\vec{w}\rangle$* (if $y\notin\textit{FV}(\vec{v})$)* 3. 3.

$\texttt{match}~{}\texttt{inl}(\vec{v})~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\vec{s}_{1}\langle x_{1}:=\vec{v}\rangle$** 4. 4.

$\texttt{match}~{}\texttt{inr}(\vec{v})~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\vec{s}_{2}\langle x_{2}:=\vec{v}\rangle$** 5. 5.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\vec{s}\,\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{s}\,\vec{t}^{\prime}$ 6. 6.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\vec{t}\,\vec{v}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}\,\vec{v}$ 7. 7.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\vec{t};\vec{s}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime};\vec{s}$ 8. 8.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\texttt{let}~{}(x_{1},x_{2})=\vec{t}~{}\texttt{in}~{}\vec{s}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}~{}\texttt{let}~{}(x_{1},x_{2})=\vec{t}^{\prime}~{}\texttt{in}~{}\vec{s}$ 9. 9.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  \begin{array}[t]{@{}l@{}}\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}~{}\mathrel{{\succ}\mskip-6.0mu{\succ}}{}\\ \qquad\texttt{match}~{}\vec{t}^{\prime}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}\\ \end{array} 10. 10.

If  $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$,  then  $\vec{t}\,\langle x:=\vec{v}\,\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}\,\langle x:=\vec{v}\,\rangle$.

Proof.

(1) Assume that $\vec{v}=\sum_{i=1}^{n}\alpha_{i}\cdot{v_{i}}$. Then we observe that

[TABLE]

(2) Assume that $\vec{v}=\sum_{i=1}^{n}\alpha_{i}\cdot{v_{i}}$ and $\vec{w}=\sum_{j=1}^{m}\beta_{j}\cdot{w_{j}}$. Then we observe that

[TABLE]

Items (3) and (4) are proved similarly as item (2). Then, items (5), (6), (7), (8), (9) and (10) are all proved following the same pattern, first treating the case where $\vec{t}\succ\vec{t}^{\prime}$ (one step), and then deducing the general case by induction on the number of evaluation steps. Let us prove for instance (5), first assuming that $\vec{t}\succ\vec{t}^{\prime}$ (one step). This means that there exist a scalar $\alpha\in\mathbb{R}$, a pure term $t_{0}$ and term distributions $\vec{t}^{\prime}_{0}$ and $\vec{r}$ such that

[TABLE]

So that for all term distributions $\vec{s}=\sum_{i=1}^{n}\beta_{i}\cdot{s_{i}}$, we have:

[TABLE]

observing that  $s_{i}\,t_{0}\mathrel{\triangleright}s_{i}\,\vec{t}^{\prime}_{0}$,  hence  $\alpha\beta_{i}\cdot s_{i}\,t_{0}+\beta_{i}\cdot s_{i}\,\vec{r}~{}\succ~{}\alpha\beta_{i}\cdot s_{i}\,\vec{t}^{\prime}_{0}+\beta_{i}\cdot s_{i}\,\vec{r}$  for all $i=1..n$. Hence we proved that $\vec{t}\succ\vec{t}^{\prime}$ implies $\vec{s}\,\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{s}\,\vec{t}^{\prime}$. By a straightforward induction on the number of evaluation steps, we deduce that $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{t}^{\prime}$ implies $\vec{s}\,\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{s}\,\vec{t}^{\prime}$. ∎

Lemma .4** (Application of realizers).**

If $\vec{s}\Vdash A\Rightarrow B$ and $\vec{t}\Vdash A$, then $\vec{s}\,\vec{t}\Vdash B$∎

Proof.

Since $\vec{t}\Vdash A$, we have $\vec{t}\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}$ for some vector $\vec{v}\in\llbracket A\rrbracket$. And since $\vec{s}\Vdash A\Rightarrow B$, we have $\vec{s}\mathrel{{\succ}\mskip-6.0mu{\succ}}\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{s}_{i}$ for some unitary distribution of abstractions $\sum_{i=1}^{n}\alpha_{i}\cdot\lambda x\,{.}\,\vec{s}_{i}\in\llbracket A\Rightarrow B\rrbracket$. Therefore, we get

[TABLE]

from Lemma .3 (5), (6), (1) and from the definition of $\llbracket A\Rightarrow B\rrbracket$. ∎

-C Proofs related to Section V

Lemma .5**.**

Given a type $A$, two vectors $\vec{u}_{1},\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$ and a scalar $\alpha\in\mathbb{C}$, there exists a vector $\vec{u}_{0}\in\llbracket\sharp{A}\rrbracket$ and a scalar $\lambda\in\mathbb{C}$ such that $\vec{u}_{1}+\alpha\cdot\vec{u}_{2}=\lambda\cdot\vec{u}_{0}$.

Proof.

Let $\lambda:=\|\vec{u}_{1}+\alpha\cdot\vec{u}_{2}\|$. When $\lambda\neq 0$, we take $\vec{u}_{0}:=\frac{1}{\lambda}\cdot(\vec{u}_{1}+\alpha\cdot\vec{u}_{2})\in\llbracket\sharp{A}\rrbracket$, and we are done. Let us now consider the (subtle) case where $\lambda=0$. In this case, we first observe that $\alpha\neq 0$, since $\alpha=0$ would imply that $\|\vec{u}_{1}+\alpha\cdot\vec{u}_{2}\|=\|\vec{u}_{1}\|=0$, which would be absurd, since $\|\vec{u}_{1}\|=1$. Moreover, since $\lambda=\|\vec{u}_{1}+\alpha\cdot\vec{u}_{2}\|=0$, we observe that all the coefficients of the distribution $\vec{u}_{1}+\alpha\cdot\vec{u}_{2}$ are zeros (when written in canonical form), which implies that

[TABLE]

Using the triangular inequality, we also observe that

[TABLE]

hence $\lambda^{\prime}:=\|\vec{u}_{1}+(-\alpha)\cdot\vec{u}_{2}\|\neq 0$. Taking $u_{0}:=\frac{1}{\lambda^{\prime}}\cdot(\vec{u}_{1}+(-\alpha)\cdot\vec{u}_{2})\in\llbracket\sharp{A}\rrbracket$, we easily see that

[TABLE]

Proposition .6** (Polarisation identity).**

For all value distributions $\vec{v}$ and $\vec{w}$, we have:

[TABLE]

Lemma .7**.**

Given a valid typing judgment of the form  $\Delta,x:\sharp{A}~{}{\vdash}~{}\vec{s}~{}{:}~{}C$,  a substitution $\sigma\in\llbracket\Delta\rrbracket$, and value distributions $\vec{u}_{1},\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$, there are value distributions $\vec{w}_{1},\vec{w}_{2}\in\llbracket C\rrbracket$ such that

[TABLE]

Proof.

From the validity of the judgment  $\Delta,x:\sharp{A}~{}{\vdash}~{}\vec{s}~{}{:}~{}C$,  we know that there are $\vec{w}_{1},\vec{w}_{2}\in\llbracket C\rrbracket$ such that $\vec{s}\langle\sigma,x:=\vec{u}_{1}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{1}$ and $\vec{s}\langle\sigma,x:=\vec{u}_{2}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{2}$. In particular, we have $\|\vec{w}_{1}\|=\|\vec{w}_{2}\|=1$. Now applying Lemma .5 four times, we know that there are vectors $\vec{u}_{0,1},\vec{u}_{0,2},\vec{u}_{0,3},\vec{u}_{0,4}\in\llbracket\sharp{A}\rrbracket$ and scalars $\lambda_{1},\lambda_{2},\lambda_{3},\lambda_{4}\in\mathbb{C}$ such that

[TABLE]

From the validity of the judgment  $\Delta,x:\sharp{A}~{}{\vdash}~{}\vec{s}~{}{:}~{}C$,  we also know that there are value distributions $\vec{w}_{0,1},\vec{w}_{0,2},\vec{w}_{0,3},\vec{w}_{0,4}\in\llbracket C\rrbracket$ such that $\vec{s}\langle\sigma,x:=\vec{u}_{0,j}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{0,j}$ for all $j=1..4$. Combining the linearity of evaluation with the uniqueness of normal forms, we deduce from what precedes that

[TABLE]

Using the polarization identity (Prop. .6), we conclude that:

[TABLE]

Lemma .8**.**

Given a valid typing judgment of the form  $\Delta,x:\sharp{A},y:\sharp{B}~{}{\vdash}~{}\vec{s}~{}{:}~{}C$,  a substitution $\sigma\in\llbracket\Delta\rrbracket$, and value distributions $\vec{u}_{1},\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$ and $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp{B}\rrbracket$ such that $\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{2}}\rangle=\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$, there are value distributions $\vec{w}_{1},\vec{w}_{2}\in\llbracket C\rrbracket$ such that

[TABLE]

Proof.

From Lemma .5, we know that there are $\vec{u}_{0}\in\llbracket\sharp{A}\rrbracket$, $\vec{v}_{0}\in\llbracket\sharp{B}\rrbracket$ and $\lambda,\mu\in\mathbb{C}$ such that

[TABLE]

For all $j,k\in\{0,1,2\}$, we have $\sigma,x:=\vec{u}_{j},y:=\vec{v}_{k}\in\llbracket\Delta,x:\sharp{A},y:\sharp{B}\rrbracket$, hence there is $\vec{w}_{j,k}\in\llbracket C\rrbracket$ such that $\vec{s}\langle\sigma,x:=\vec{u}_{j},y:=\vec{v}_{k}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{j,k}$. In particular, we can take $\vec{w}_{1}:=\vec{w}_{1,1}$ and $\vec{w}_{2}:=\vec{w}_{2,2}$. Now, we observe that

$\vec{u}_{1}+\lambda\cdot\vec{u}_{0}=\vec{u}_{1}+\vec{u}_{2}+(-1)\cdot\vec{u}_{1}=\vec{u}_{2}+0\cdot\vec{u}_{1}$, so that from the linearity of substitution, the linearity of evaluation and from the uniqueness of normal forms, we get

as well as \begin{array}[b]{r@{~{}~}c@{~{}~}l}\vec{w}_{1,k}+\lambda\cdot\vec{w}_{0,k}~{}{}&=\hfil~{}{}&\vec{w}_{2,k}+0\cdot\vec{w}_{1,k}\\ \vec{w}_{2,k}+(-\lambda)\cdot\vec{w}_{0,k}~{}{}&=\hfil~{}{}&\vec{w}_{1,k}+0\cdot\vec{w}_{2,k}\\ \end{array} (for all $k\in\{0,1,2\}$) 2. 2.

$\vec{v}_{1}+\mu\cdot\vec{v}_{0}=\vec{v}_{1}+\vec{v}_{2}+(-1)\cdot\vec{v}_{1}=\vec{v}_{2}+0\cdot\vec{v}_{1}$, so that from the linearity of substitution, the linearity of evaluation and from the uniqueness of normal forms, we get

as well as \begin{array}[b]{r@{~{}~}c@{~{}~}l}\vec{w}_{j,1}+\mu\cdot\vec{w}_{j,0}~{}{}&=\hfil~{}{}&\vec{w}_{j,2}+0\cdot\vec{w}_{j,1}\\ \vec{w}_{j,2}+(-\mu)\cdot\vec{w}_{j,0}~{}{}&=\hfil~{}{}&\vec{w}_{j,1}+0\cdot\vec{w}_{j,2}\\ \end{array} (for all $j\in\{0,1,2\}$) 3. 3.

$\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{2}}\rangle=0$, so that from Lemma .7 we get $\langle{\vec{w}_{1,k}}~{}|~{}{\vec{w}_{2,k}}\rangle~{}=~{}0$ (for all $k\in\{0,1,2\}$) 4. 4.

$\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle=0$, so that from Lemma .7 we get $\langle{\vec{w}_{j,1}}~{}|~{}{\vec{w}_{j,2}}\rangle~{}=~{}0$ (for all $j\in\{0,1,2\}$)

From the above, we get:

[TABLE]

Hence $\langle{\vec{w}_{1}}~{}|~{}{\vec{w}_{2}}\rangle=\langle{\vec{w}_{1,1}}~{}|~{}{\vec{w}_{2,2}}\rangle=-\langle{\vec{w}_{2,1}}~{}|~{}{\vec{w}_{1,2}}\rangle$. Exchanging the indices $j$ and $k$ in the above reasoning, we also get $\langle{\vec{w}_{1}}~{}|~{}{\vec{w}_{2}}\rangle=\langle{\vec{w}_{1,1}}~{}|~{}{\vec{w}_{2,2}}\rangle=-\langle{\vec{w}_{1,2}}~{}|~{}{\vec{w}_{2,1}}\rangle$, so that we have $\langle{\vec{w}_{1}}~{}|~{}{\vec{w}_{2}}\rangle=-\langle{\vec{w}_{2,1}}~{}|~{}{\vec{w}_{1,2}}\rangle=-\overline{\langle{\vec{w}_{2,1}}~{}|~{}{\vec{w}_{1,2}}\rangle}\in\mathbb{R}$. If we now replace $\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$ with $i\,\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$, the very same technique allows us to prove that $i\langle{\vec{w}_{1}}~{}|~{}{\vec{w}_{2}}\rangle=\langle{\vec{w}_{1}}~{}|~{}{i\vec{w}_{2}}\rangle\in\mathbb{R}$. Therefore $\langle{\vec{w}_{1}}~{}|~{}{\vec{w}_{2}}\rangle=0$. ∎

Lemma .9**.**

Given a valid typing judgment of the form  $\Delta,x:\sharp{A},y:\sharp{B}~{}{\vdash}~{}\vec{s}~{}{:}~{}C$,  a substitution $\sigma\in\llbracket\Delta\rrbracket$, and value distributions $\vec{u}_{1},\vec{u}_{2}\in\llbracket\sharp{A}\rrbracket$ and $\vec{v}_{1},\vec{v}_{2}\in\llbracket\sharp{B}\rrbracket$, there are value distributions $\vec{w}_{1},\vec{w}_{2}\in\llbracket C\rrbracket$ such that

[TABLE]

Proof.

Let $\alpha=\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{2}}\rangle$ and $\beta=\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}}\rangle$. We observe that

[TABLE]

and, similarly, that $\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}+(-\beta)\cdot\vec{v}_{1}}\rangle=0$. From Lemma .5, we know that there are $\vec{u}_{0}\in\llbracket\sharp{A}\rrbracket$, $\vec{v}_{0}\in\llbracket\sharp{B}\rrbracket$ and $\lambda,\mu\in\mathbb{C}$ such that

[TABLE]

For all $j,k\in\{0,1,2\}$, we have $\sigma,x:=\vec{u}_{j},y:=\vec{v}_{k}\in\llbracket\Delta,x:\sharp{A},y:\sharp{B}\rrbracket$, hence there is $\vec{w}_{j,k}\in\llbracket C\rrbracket$ such that $\vec{s}\langle\sigma,x:=\vec{u}_{j},y:=\vec{v}_{k}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{j,k}$. In particular, we can take $\vec{w}_{1}:=\vec{w}_{1,1}$ and $\vec{w}_{2}:=\vec{w}_{2,2}$. Now, we observe that

$\lambda\cdot\vec{u}_{0}+\alpha\cdot\vec{u}_{1}=\vec{u}_{2}+(-\alpha)\cdot\vec{u}_{1}+\alpha\cdot\vec{u}_{1}=\vec{u}_{2}+0\cdot\vec{u}_{1}$, so that from the linearity of substitution, the linearity of evaluation and from the uniqueness of normal forms, we get

[TABLE] 2. 2.

$\mu\cdot\vec{v}_{0}+\beta\cdot\vec{v}_{1}=\vec{v}_{2}+(-\beta)\cdot\vec{v}_{1}+\beta\cdot\vec{v}_{1}=\vec{v}_{2}+0\cdot\vec{v}_{1}$, so that from the linearity of substitution, the linearity of evaluation and from the uniqueness of normal forms, we get

[TABLE] 3. 3.

$\langle{\vec{u}_{1}}~{}|~{}{\lambda\cdot\vec{u}_{0}}\rangle=\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{2}+(-\alpha)\cdot\vec{u}_{1}}\rangle=0$, so that from Lemma .7 we get

[TABLE]

(The equality $\langle{\vec{w}_{1,k}}~{}|~{}{\lambda\cdot\vec{w}_{0,k}}\rangle=0$ is trivial when $\lambda=0$, and when $\lambda\neq 0$, we deduce from the above that $\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{0}}\rangle=0$, from which we get $\langle{\vec{w}_{1,k}}~{}|~{}{\vec{w}_{0,k}}\rangle=0$ by Lemma .7.) 4. 4.

$\langle{\vec{v}_{1}}~{}|~{}{\mu\cdot\vec{v}_{0}}\rangle=\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{2}+(-\beta)\cdot\vec{v}_{1}}\rangle=0$, so that from Lemma .7 we get

[TABLE] 5. 5.

$\langle{\vec{u}_{1}}~{}|~{}{\lambda\cdot\vec{u}_{0}}\rangle=\langle{\vec{v}_{1}}~{}|~{}{\mu\cdot\vec{v}_{0}}\rangle=0$, so that from Lemma .8 we get

[TABLE]

(Again, the equality $\langle{\vec{w}_{1,1}}~{}|~{}{\lambda\mu\cdot\vec{w}_{0,0}}\rangle=0$ is trivial when $\lambda=0$ or $\mu=0$, and when $\lambda,\mu\neq 0$, we deduce from the above that $\langle{\vec{u}_{1}}~{}|~{}{\vec{u}_{0}}\rangle=\langle{\vec{v}_{1}}~{}|~{}{\vec{v}_{0}}\rangle=0$, from which we get $\langle{\vec{w}_{1,1}}~{}|~{}{\vec{w}_{0,0}}\rangle=0$ by Lemma .8.)

From the above, we get

[TABLE]

Therefore:

[TABLE]

from (5), (3) (with $k=1$) and (4) (with $j=1$), and concluding with the definition of $\alpha$ and $\beta$. ∎

Lemma .10**.**

For all $\vec{t},\vec{s},\vec{s}_{1},\vec{s}_{2}\in\vec{\Lambda}(\mathcal{X})$ and $\vec{v},\vec{v}_{1},\vec{v}_{2},\vec{w}\in\vec{\mathrm{V}}(\mathcal{X})$:

$\texttt{inl}(\vec{v})\langle x:=\vec{w}\rangle~{}=~{}\texttt{inl}(\vec{v}\langle x:=\vec{w}\rangle)$** 2. 2.

$\texttt{inr}(\vec{v})\langle x:=\vec{w}\rangle~{}=~{}\texttt{inr}(\vec{v}\langle x:=\vec{w}\rangle)$** 3. 3.

If $x\notin\textit{FV}(\vec{v}_{1})$, then $(\vec{v}_{1},\vec{v}_{2})\langle x:=\vec{w}\rangle~{}=~{}(\vec{v}_{1},\vec{v}_{2}\langle x:=\vec{w}\rangle)$ 4. 4.

If $x\notin\textit{FV}(\vec{v}_{2})$, then $(\vec{v}_{1},\vec{v}_{2})\langle x:=\vec{w}\rangle~{}=~{}(\vec{v}_{1}\langle x:=\vec{w}\rangle,\vec{v}_{2})$ 5. 5.

If $x\notin\textit{FV}(\vec{s})$, then $(\vec{s}\,\vec{t})\langle x:=\vec{w}\rangle~{}=~{}\vec{s}~{}\vec{t}\langle x:=\vec{w}\rangle$ 6. 6.

If $x\notin\textit{FV}(\vec{t})$, then $(\vec{s}\,\vec{t})\langle x:=\vec{w}\,\rangle~{}=~{}\vec{s}\langle x:=\vec{w}\rangle~{}\vec{t}$ 7. 7.

If $x\notin\textit{FV}(\vec{s})$, then $(\vec{t};\vec{s})\langle x:=\vec{w}\rangle~{}=~{}\vec{t}\langle x:=\vec{w}\rangle;\vec{s}$ 8. 8.

If $x\notin\textit{FV}(\vec{s})$, then $(\texttt{let}~{}(x_{1},x_{2})=\vec{t}~{}\texttt{in}~{}\vec{s})\langle x:=\vec{w}\rangle~{}=~{}\texttt{let}~{}(x_{1},x_{2})=\vec{t}\langle x:=\vec{w}\rangle~{}\texttt{in}~{}\vec{s}$ 9. 9.

If $x\notin\textit{FV}(\vec{s}_{1},\vec{s}_{2})$, then $(\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\})\langle x:=\vec{w}\rangle~{}={}\texttt{match}~{}\vec{t}\langle x:=\vec{w}\rangle~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\}$

∎

Proposition V.3. The typing rules of Table VI are valid.

Proof.

(Axiom) It is clear that $\mathrm{dom}^{\sharp}(x:A)\subseteq\{x\}=\mathrm{dom}(x:A)$. Moreover, given $\sigma\in\llbracket x:A\rrbracket$, we have $\sigma=\{x:=\vec{v}\}$ for some $\vec{v}\in\llbracket A\rrbracket$. Therefore $x\langle\sigma\rangle=x\langle x:=\vec{v}\rangle=\vec{v}\Vdash A$.

(Sub) Obvious since $\{{\Vdash}~{}A\}\subseteq\{{\Vdash}~{}A^{\prime}\}$.

(App) Suppose that both judgments $\Gamma~{}{\vdash}~{}\vec{s}~{}{:}~{}A\Rightarrow B$ and $\Delta~{}{\vdash}~{}\vec{t}~{}{:}~{}A$ are valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{s}\,)\subseteq\mathrm{dom}(\Gamma)$ and $\vec{s}\,\langle\sigma\rangle\Vdash A\Rightarrow B$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• $\bullet$

$\mathrm{dom}^{\sharp}(\Delta)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Delta)$ and $\vec{t}\,\langle\sigma\rangle\Vdash A$  for all $\sigma\in\llbracket\Delta\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\vec{s}~{}\vec{t}\,)\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. And since $\textit{FV}(\vec{t}\,)\cap\mathrm{dom}(\sigma_{\Gamma})=\varnothing$ and $\textit{FV}(\vec{s}\,)\cap\mathrm{dom}(\sigma_{\Delta})=\varnothing$, we deduce from Lemma .10 (5), (6) p. .10 that

[TABLE]

We conclude that  $(\vec{s}~{}\vec{t}\,)\langle\sigma\rangle=\vec{s}\langle\sigma_{\Gamma}\rangle~{}\vec{t}\langle\sigma_{\Delta}\rangle\Vdash B$  from Lemma .4.

(PureLam) Given a context $\Gamma=x_{1}:A_{1},\ldots,x_{\ell}:A_{\ell}$ such that $\flat{A_{i}}\simeq A_{i}$ for all $i=1..\ell$, we suppose that the judgment $\Gamma,x:A~{}{\vdash}~{}\vec{t}~{}{:}~{}B$ is valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma,x:A)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma,x:A)$ and $\vec{t}\,\langle\sigma\rangle\Vdash B$  for all $\sigma\in\llbracket\Gamma,x:A\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\lambda x\,{.}\,\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$. Now, given $\sigma\in\llbracket\Gamma\rrbracket$, we want to prove that $(\lambda x\,{.}\,\vec{t}\,)\langle\sigma\rangle\Vdash A\rightarrow B$. Due to our initial assumption on the context $\Gamma$, it is clear that $\sigma=\{x_{1}:=v_{1},\ldots,x_{\ell}:=v_{\ell}\}$ for some closed pure values $v_{1},\ldots,v_{\ell}$. Hence

[TABLE]

(since the variables $x_{1},\ldots,x_{\ell}$ are all distinct from $x$). For all $\vec{v}\in\llbracket A\rrbracket$, we observe that

[TABLE]

since $\sigma,\{x:=\vec{v}\,\}\in\llbracket\Gamma,x:A\rrbracket$. Therefore $(\lambda x\,{.}\,\vec{t}\,)\langle\sigma\rangle\Vdash A\rightarrow B$.

(UnitLam) Suppose that the judgment $\Gamma,x:A~{}{\vdash}~{}\vec{t}~{}{:}~{}B$ is valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma,x:A)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma,x:A)$ and $\vec{t}\,\langle\sigma\rangle\Vdash B$  for all $\sigma\in\llbracket\Gamma,x:A\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\lambda x\,{.}\,\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$. Now, given $\sigma\in\llbracket\Gamma\rrbracket$, we want to prove that $(\lambda x\,{.}\,\vec{t}\,)\langle\sigma\rangle\Vdash A\Rightarrow B$. For that, we write:

• •

$\Gamma=x_{1}:A_{1},\ldots,x_{\ell}:A_{\ell}$ (where $x_{1},\ldots,x_{\ell}$ are all distinct from $x$);

• •

$\sigma=\{x_{1}:=\vec{v}_{1},\ldots,x_{\ell}:=\vec{v}_{\ell}\}$ (where $\vec{v}_{i}\in\llbracket A_{i}\rrbracket$ for all $i=1..\ell$);

• •

$\vec{v}_{i}=\sum_{j=1}^{n_{i}}\alpha_{i,j}\cdot{v_{i,j}}$ (in canonical form) for all $i=1..\ell$.

Now we observe that

[TABLE]

writing

• •

$I:=[1..n_{1}]\times\cdots\times[1..n_{\ell}]$  the (finite) set of all multi-indices $i=(i_{1},\ldots,i_{\ell})$;

• •

$\alpha_{i}:=\alpha_{1,i_{1}}\cdots\alpha_{\ell,i_{\ell}}$  and  $\vec{t}_{i}:=\vec{t}\,[x_{1}:=v_{1,i_{1}}]\cdots[x_{\ell}:=v_{\ell,i_{\ell}}]$  for each multi-index

$i=(i_{1},\ldots,i_{\ell})\in I$.

We now want to prove that \bigl{(}\sum_{i\in I}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1}. For that, we first observe that

[TABLE]

Then we need to check that the $\lambda$-abstractions  $\lambda x\,{.}\,\vec{t}_{i}$  ($i\in I$) are pairwise distinct. For that, consider two multi-indices $i=(i_{1},\ldots,i_{\ell})$ and $i^{\prime}=(i^{\prime}_{1},\ldots,i^{\prime}_{\ell})$ such that $i\neq i^{\prime}$. This means that $i_{k}\neq i^{\prime}_{k}$ for some $k\in[1..\ell]$. From the latter, we deduce that $n_{k}\geq 2$, hence $\vec{v}_{k}=\sum_{j=1}^{n_{k}}\alpha_{k,j}\cdot{v_{k,j}}$ is not a pure value, and thus $\llbracket A_{k}\rrbracket\neq\flat\llbracket A_{k}\rrbracket$. Therefore $x_{k}\in\mathrm{dom}^{\sharp}(\Gamma)$, from which we deduce that $x_{k}\in\textit{FV}(\vec{t}\,)$ from our initial assumption. Let us now consider the first occurrence of the variable $x_{k}$ in the (raw) term distribution $\vec{t}$. At this occurrence, the variable $x_{k}$ is replaced

• •

by $v_{k,i_{k}}$ in the multiple substitution $\vec{t}\,[x_{1}:=v_{1,i_{1}}]\cdots[x_{\ell}:=v_{\ell,i_{\ell}}]~{}({=}~{}\vec{t}_{i})$, and

• •

by $v_{k,i^{\prime}_{k}}$ in the multiple substitution $\vec{t}\,[x_{1}:=v_{1,i^{\prime}_{1}}]\cdots[x_{\ell}:=v_{\ell,i^{\prime}_{\ell}}]~{}({=}~{}\vec{t}_{i^{\prime}})$.

And since $v_{k,i_{k}}\neq v_{k,i^{\prime}_{k}}$ (recall that $\vec{v}_{k}=\sum_{j=1}^{n_{k}}\alpha_{k,j}\cdot v_{k,j}$ is in canonical form), we deduce that $\vec{t}_{i}\neq\vec{t}_{i^{\prime}}$. Which concludes the proof that \bigl{(}\sum_{i\in I}\alpha_{i}\cdot\lambda x\,{.}\,\vec{t}_{i}\bigr{)}\in\mathcal{S}_{1}. Now, given $\vec{v}\in\llbracket A\rrbracket$, it remains to show that $\sum_{i\in I}\alpha_{i}\cdot\vec{t}_{i}\langle x:=\vec{v}\rangle\Vdash B$. For that, it suffices to observe that:

[TABLE]

since $\sigma,\{x:=\vec{v}\,\}\in\llbracket\Gamma,x:A\rrbracket$. Therefore $(\lambda x\,{.}\,\vec{t}\,)\langle\sigma\rangle=\sum_{i\in I}\alpha_{i}\cdot\vec{t}_{i}\in\llbracket A\Rightarrow B\rrbracket\subseteq\{{\Vdash}~{}A\Rightarrow B\}$.

(Void) Obvious.

(Seq) Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}\mathbb{U}$ and $\Delta~{}{\vdash}~{}\vec{s}~{}{:}~{}A$ are valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}*$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• $\bullet$

$\mathrm{dom}^{\sharp}(\Delta)\subseteq\textit{FV}(\vec{s})\subseteq\mathrm{dom}(\Delta)$ and $\vec{s}\langle\sigma\rangle\Vdash A$  for all $\sigma\in\llbracket\Delta\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\vec{t};\vec{s})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. From our initial hypotheses, we get

[TABLE]

(using Lemma .10 (7) p. .10 and Lemma .3 (7), (10) p. .3).

(SeqSharp) Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}\sharp\mathbb{U}$ and $\Delta~{}{\vdash}~{}\vec{s}~{}{:}~{}\sharp{A}$ are valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash\sharp\mathbb{U}$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• $\bullet$

$\mathrm{dom}^{\sharp}(\Delta)\subseteq\textit{FV}(\vec{s})\subseteq\mathrm{dom}(\Delta)$ and $\vec{s}\langle\sigma\rangle\Vdash\sharp{A}$  for all $\sigma\in\llbracket\Delta\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\vec{t};\vec{s})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. From our first hypothesis, we get $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot*$ for some $\alpha\in\mathbb{C}$ such that $|\alpha|=1$. And from the second hypothesis, we have $\vec{s}\langle\sigma_{\Delta}\rangle\Vdash\sharp{A}$, and thus $\alpha\cdot\vec{s}\langle\sigma_{\Delta}\rangle\Vdash\sharp{A}$ (since $|\alpha|=1$). Therefore, we get

[TABLE]

(using Lemma .10 (7) p. .10 and Lemma .3 (7), (10) p. .3).

(Pair) Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{v}~{}{:}~{}A$ and $\Delta~{}{\vdash}~{}\vec{w}~{}{:}~{}B$ are valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{v})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{v}\langle\sigma\rangle\Vdash A$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• $\bullet$

$\mathrm{dom}^{\sharp}(\Delta)\subseteq\textit{FV}(\vec{w})\subseteq\mathrm{dom}(\Delta)$ and $\vec{w}\langle\sigma\rangle\Vdash B$  for all $\sigma\in\llbracket\Delta\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}((\vec{v},\vec{w}))\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. From our initial hypotheses, we deduce that $\vec{v}\langle\sigma_{\Gamma}\rangle\Vdash A$ and $\vec{w}\langle\sigma_{\Delta}\rangle\Vdash B$, which means that $\vec{v}\langle\sigma_{\Gamma}\rangle\in\llbracket A\rrbracket$ and $\vec{w}\langle\sigma_{\Delta}\rangle\in\llbracket B\rrbracket$ (from Lemma IV.3), since $\vec{v}\langle\sigma_{\Gamma}\rangle$ and $\vec{w}\langle\sigma_{\Delta}\rangle$ are value distributions. And since $\textit{FV}(\vec{v})\cap\mathrm{dom}(\sigma_{\Delta})=\varnothing$ and $\textit{FV}(\vec{w})\cap\mathrm{dom}(\sigma_{\Gamma})=\varnothing$, we deduce from Lemma .10 (3), (4) p. .10 that

[TABLE]

from the definition of $\llbracket A\times B\rrbracket$.

(LetPair) Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A\times B$ and $\Delta,x:A,y:B~{}{\vdash}~{}\vec{s}~{}{:}~{}C$ are valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash A\times B$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• $\bullet$

$\mathrm{dom}^{\sharp}(\Delta,x:A,y:B)\subseteq\textit{FV}(\vec{s})\subseteq\mathrm{dom}(\Delta,x:A,y:B)$ and

$\vec{s}\langle\sigma\rangle\Vdash C$  for all $\sigma\in\llbracket\Delta,x:A,y:B\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\texttt{let}~{}(x,y)=\vec{t}~{}\texttt{in}~{}\vec{s})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. Since $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$, we know from our first hypothesis that $\vec{t}\langle\sigma_{\Gamma}\rangle\Vdash A\times B$, which means that $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}(\vec{v},\vec{w})$ for some $\vec{v}\in\llbracket A\rrbracket$ and $\vec{w}\in\llbracket B\rrbracket$. So that we get

[TABLE]

using our second hypothesis with the substitution $\sigma_{\Delta},\{x:=\vec{v},y:=\vec{w}\}\in\llbracket\Delta,x:A,y:B\rrbracket$.

(LetTens) Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A\otimes B$ and $\Delta,x:\sharp{A},y:\sharp{B}~{}{\vdash}~{}\vec{s}~{}{:}~{}\sharp C$ are valid, that is:

• •

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash A\otimes B$ for all $\sigma\in\llbracket\Gamma\rrbracket$.

• •

$\mathrm{dom}^{\sharp}(\Delta,x:\sharp{A},y:\sharp{B})\subseteq\textit{FV}(\vec{s})\subseteq\mathrm{dom}(\Delta,x:\sharp{A},y:\sharp{B})$ and

$\vec{s}\langle\sigma\rangle\Vdash\sharp{C}$ for all $\sigma\in\llbracket\Delta,x:\sharp{A},y:\sharp{B}\rrbracket$

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\texttt{let}~{}(x,y)=\vec{t}~{}\texttt{in}~{}\vec{s})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. Since $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$, we know from our first hypothesis that $\vec{t}\langle\sigma_{\Gamma}\rangle\Vdash A\otimes B$, which means that $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\sum_{i=1}^{n}\alpha_{i}\cdot(\vec{u}_{i},\vec{v}_{i})$ for some $\alpha_{1},\ldots,\alpha_{n}\in\mathbb{C}$, $\vec{u}_{1},\ldots,\vec{u}_{n}\in\llbracket A\rrbracket$ and $\vec{v}_{1},\ldots,\vec{v}_{n}\in\llbracket B\rrbracket$, with \bigl{\|}\sum_{i=1}^{n}\alpha_{i}\cdot(\vec{u}_{i},\vec{v}_{i})\bigr{\|}=1. For each $i=1..n$, we also observe that $\sigma_{\Delta},x:=\vec{u}_{i},y:=\vec{v}_{i}\in\llbracket\Delta,x:\sharp{A},y:\sharp{B}\rrbracket$. From our second hypothesis, we get $\vec{s}\langle\sigma_{\Delta},x:=\vec{u}_{i},y:=\vec{v}_{i}\rangle\Vdash\sharp{C}$, hence there is $\vec{w}_{i}\in\llbracket\sharp{C}\rrbracket$ such that $\vec{s}\langle\sigma_{\Delta},x:=\vec{u}_{i},y:=\vec{v}_{i}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{w}_{i}$. Therefore, we have:

[TABLE]

To conclude, it remains to show that \bigl{\|}\sum_{i=1}^{n}\alpha_{i}\cdot\vec{w}_{i}\bigr{\|}=1. For that, we observe that:

[TABLE]

(InL) Suppose that the judgment $\Gamma~{}{\vdash}~{}\vec{v}~{}{:}~{}A$ is valid, that is:

• $\bullet$

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{v})\subseteq\mathrm{dom}(\Gamma)$ and $\vec{v}\langle\sigma\rangle\Vdash A$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\texttt{inl}(\vec{v}))\subseteq\mathrm{dom}(\Gamma)$. Now, given $\sigma\in\llbracket\Gamma\rrbracket$, we know that $\vec{v}\langle\sigma\rangle\Vdash A$, which means that $\vec{v}\langle\sigma\rangle\in\llbracket A\rrbracket$ (by Lemma IV.3), since $\vec{v}\langle\sigma\rangle$ is a value distribution. So that by Lemma .10 (1), we conclude that $\texttt{inl}(\vec{v})\langle\sigma\rangle=\texttt{inl}(\vec{v}\langle\sigma\rangle)\in\llbracket A+B\rrbracket$.

(InR) Analogous to (InL).

(PureMatch) Suppose that the judgments  $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A+B$,  $\Delta,x_{1}:A~{}{\vdash}~{}\vec{s}_{1}~{}{:}~{}C$  and  $\Delta,x_{2}:B~{}{\vdash}~{}\vec{s}_{2}~{}{:}~{}C$  are valid, that is:

• •

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash A+B$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

• •

$\mathrm{dom}^{\sharp}(\Delta,x_{1}:A)\subseteq\textit{FV}(\vec{s}_{1})\subseteq\mathrm{dom}(\Delta,x_{1}:A)$ and $\vec{s}_{1}\langle\sigma\rangle\Vdash C$  for all $\sigma\in\llbracket\Delta,x_{1}:A\rrbracket$.

• •

$\mathrm{dom}^{\sharp}(\Delta,x_{2}:B)\subseteq\textit{FV}(\vec{s}_{2})\subseteq\mathrm{dom}(\Delta,x_{2}:B)$ and $\vec{s}_{2}\langle\sigma\rangle\Vdash C$  for all $\sigma\in\llbracket\Delta,x_{2}:B\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given a substitution $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. And since $\textit{FV}(\vec{s}_{1},\vec{s}_{2})\cap\mathrm{dom}(\sigma_{\Gamma})=\varnothing$, we deduce from Lemma .10 (9) that

[TABLE]

Moreover, since $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$, we have $\vec{t}\langle\sigma_{\Gamma}\rangle\Vdash A+B$ (from our first hypothesis), so that we distinguish the following two cases:

• •

Either $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\texttt{inl}(\vec{v})$ for some $\vec{v}\in\llbracket A\rrbracket$, so that

[TABLE]

using our second hypothesis with the substitution $\sigma_{\Delta},\{x_{1}:=\vec{v}\}\in\llbracket\Delta,x_{1}:A\rrbracket$.

• •

Either $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\texttt{inr}(\vec{w})$ for some $\vec{w}\in\llbracket B\rrbracket$, so that

[TABLE]

using our third hypothesis with the substitution $\sigma_{\Delta},\{x_{2}:=\vec{w}\}\in\llbracket\Delta,x_{2}:B\rrbracket$.

(Weak) Suppose that the judgment $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}B$ is valid, that is

• •

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash B$  for all $\sigma\in\llbracket\Gamma\rrbracket$.

Given a type $A$ such that $\flat{A}\simeq A$, it is clear from the above that $\mathrm{dom}^{\sharp}(\Gamma,x:A)~{}({=}~{}\mathrm{dom}^{\sharp}(\Gamma))\subseteq\textit{FV}(\vec{t})\subseteq\mathrm{dom}(\Gamma,x:A)$. Now, given $\sigma\in\llbracket\Gamma,x:A\rrbracket$, we observe that $\sigma=\sigma_{0},\{x:=v\}$ for some substitution $\sigma_{0}\in\llbracket\Gamma\rrbracket$ and for some pure value $v\in\llbracket A\rrbracket~{}({=}~{}\flat\llbracket A\rrbracket)$. Therefore, we get

[TABLE]

(Contr) Given a type $A$ such that $\flat{A}\simeq A$, suppose that $\Gamma,x:A,y:A~{}{\vdash}~{}\vec{t}~{}{:}~{}B$, that is:

• •

$\mathrm{dom}^{\sharp}(\Gamma,x:A,y:A)~{}({=}~{}\mathrm{dom}^{\sharp}(\Gamma))\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma,x:A,y:A)$

and $\vec{t}\langle\sigma\rangle\Vdash B$  for all $\sigma\in\llbracket\Gamma,x:A,y:A\rrbracket$.

From the above, it is clear that $\mathrm{dom}^{\sharp}(\Gamma,x:A)~{}({=}~{}\mathrm{dom}^{\sharp}(\Gamma))\subseteq\textit{FV}(\vec{t}\,[y:=x])\subseteq\mathrm{dom}(\Gamma,x:A)$. Now, given $\sigma\in\llbracket\Gamma,x:A\rrbracket$, we observe that $\sigma=\sigma_{0},\{x:=v\}$ for some substitution $\sigma_{0}\in\llbracket\Gamma\rrbracket$ and for some pure value $v\in\llbracket A\rrbracket~{}({=}~{}\flat\llbracket A\rrbracket)$. Therefore, we have

[TABLE]

since $\sigma_{0},\{x:=v,y:=v\}\in\llbracket\Gamma,x:A,y:A\rrbracket$. ∎

Fact .11**.**

For all $n\neq 1$, one has: $\bar{n}\not\Vdash(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})\Rightarrow(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})$.

Proof.

Let F:=\frac{3}{5}\cdot\bigl{(}\lambda x\,{.}\,\frac{5}{6}\cdot x\bigr{)}+\frac{4}{5}\cdot\bigl{(}\lambda x\,{.}\,\frac{5}{8}\cdot x\bigr{)}. We observe that \bigl{|}\frac{3}{5}\bigr{|}^{2}+\bigl{|}\frac{4}{5}\bigr{|}^{2}=\frac{9+16}{25}=1. Moreover, for all $\vec{v}\in\llbracket\mathbb{B}\rrbracket$, we have

[TABLE]

hence $F\Vdash\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$. Now, we observe that when $n\neq 1$, we have

[TABLE]

since  \frac{3}{5}\bigl{(}\frac{5}{6}\bigr{)}^{n}+\frac{4}{5}\bigl{(}\frac{5}{8}\bigr{)}^{n}=\frac{7}{5}>1  when $n=0$  and  \frac{3}{5}\bigl{(}\frac{5}{6}\bigr{)}^{n}+\frac{4}{5}\bigl{(}\frac{5}{8}\bigr{)}^{n}<\frac{3}{5}\cdot\frac{5}{6}+\frac{4}{5}\cdot\frac{5}{8}=1  when $n\geq 2$. Hence $\bar{n}\,F\,\mathtt{t\!t}\not\Vdash\sharp\mathbb{B}$, and therefore  $\bar{n}\not\Vdash(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})\Rightarrow(\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B})$. ∎

Proposition V.7. * The rule (UnitaryMatch) is valid. *

Proof.

Suppose that the judgments $\Gamma~{}{\vdash}~{}\vec{t}~{}{:}~{}A_{1}\oplus A_{2}$ and $\Delta~{}{\vdash}~{}(x_{1}:\sharp A_{1}~{}{\vdash}~{}\vec{s}_{1})\perp(x_{2}:\sharp A_{2}~{}{\vdash}~{}\vec{s}_{2})~{}{:}~{}\sharp C$ are valid, that is:

• •

$\mathrm{dom}^{\sharp}(\Gamma)\subseteq\textit{FV}(\vec{t}\,)\subseteq\mathrm{dom}(\Gamma)$ and $\vec{t}\langle\sigma\rangle\Vdash A_{1}\oplus A_{2}$ for all $\sigma\in\llbracket\Gamma\rrbracket$.

• •

For $i=1,2$, $\mathrm{dom}^{\sharp}(\Delta,x_{i}:\sharp A_{i})\subseteq\textit{FV}(\vec{s}_{i}\,)\subseteq\mathrm{dom}(\Delta,x_{i}:\sharp A_{i})$ and $\vec{s}_{i}\langle\sigma,\sigma_{i}\rangle\Vdash\sharp C$ for all $\sigma\in\llbracket\Delta\rrbracket$ and $\sigma_{i}\in\llbracket x_{i}:\sharp A_{i}\rrbracket$.

• •

For $i=1,2$, $\vec{s}_{i}\langle\sigma,\sigma_{i}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\vec{v}_{i}$ with $\langle\vec{v}_{1}|\vec{v}_{2}\rangle=0$.

From the above, it is clear the $\mathrm{dom}^{\sharp}(\Gamma,\Delta)\subseteq\textit{FV}(\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\})\subseteq\mathrm{dom}(\Gamma,\Delta)$. Now, given a substitution $\sigma\in\llbracket\Gamma,\Delta\rrbracket$, we observe that $\sigma=\sigma_{\Gamma},\sigma_{\Delta}$ for some $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$ and $\sigma_{\Delta}\in\llbracket\Delta\rrbracket$. And since $FV(\vec{s}_{1},\vec{s}_{2})\cap\mathrm{dom}(\sigma_{\Gamma})=\varnothing$, we deduce from Lemma .10 (8) that

[TABLE]

Moreover, since $\sigma_{\Gamma}\in\llbracket\Gamma\rrbracket$, we have $\vec{t}\langle\sigma_{\Gamma}\rangle\Vdash A_{1}\oplus A_{2}$ (from our first hypothesis), so that we have $\vec{t}\langle\sigma_{\Gamma}\rangle\mathrel{{\succ}\mskip-6.0mu{\succ}}\alpha\cdot\texttt{inl}(\vec{v}_{1})+\beta\cdot\texttt{inr}(\vec{v}_{2})$ for some $\vec{v}_{1}\in\llbracket A_{1}\rrbracket$ and $\vec{v}_{2}\in\llbracket A_{2}\rrbracket$. Therefore

[TABLE]

using the last two hypotheses, with the substitution $\sigma_{\Delta},\langle x_{i}:=\vec{v}_{i}\rangle\in\llbracket\Delta,x_{i}:\sharp A_{i}\rrbracket$. ∎

-D Proofs related to Section VI

Typing rules of the standard judgements for $\lambda_{Q}$

[TABLE]

Lemma VI.2. For all classical types $A$, $\flat\llparenthesis{A}\rrparenthesis\simeq\llparenthesis{A}\rrparenthesis$.

Proof.

We proceed by structural induction on $A$.

• •

$\llparenthesis{\mathbb{U}}\rrparenthesis=\mathbb{U}=\{*\}\simeq\flat\{*\}=\flat\mathbb{U}$.

• •

$\llparenthesis{A\to B}\rrparenthesis=\llparenthesis{A}\rrparenthesis\to\llparenthesis{B}\rrparenthesis\simeq\flat(\llparenthesis{A}\rrparenthesis\to\llparenthesis{B}\rrparenthesis)$ by rule (FlatPureArrow).

• •

$\llparenthesis{A\times B}\rrparenthesis=\llparenthesis{A}\rrparenthesis\times\llparenthesis{B}\rrparenthesis\simeq\flat\llparenthesis{A}\rrparenthesis\times\flat\llparenthesis{B}\rrparenthesis\simeq\flat(\llparenthesis{A}\rrparenthesis\times\llparenthesis{B}\rrparenthesis)$, using the induction hypothesis and rules (ProdMono) and (FlatProd).

• •

$\llparenthesis{\mathsf{bit}}\rrparenthesis=\mathbb{B}=\mathbb{U}+\mathbb{U}=\flat\mathbb{U}+\flat\mathbb{U}=\flat(\mathbb{U}+\mathbb{U})=\flat\llparenthesis{\mathsf{bit}}\rrparenthesis$ using rules (SumMono) and (FlatSum).

• •

$\llparenthesis{A_{Q}\multimap B_{Q}}\rrparenthesis=\mathbb{U}\to(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis)\simeq\flat(\mathbb{U}\to(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis))$ by rule (FlatPureArrow). ∎

Lemma VI.3. For all qbit types $A_{Q}$, $\sharp\llparenthesis{A_{Q}}\rrparenthesis\simeq\llparenthesis{A_{Q}}\rrparenthesis$.

Proof.

First notice that for any $A$ from the unitary linear algebraic lambda-calculs, we have $\sharp A\simeq\sharp\sharp A$. Indeed, by rule (SharpIntro) $\sharp A\leq\sharp\sharp A$, and by rules (SubRefl) and (SharpLift), $\sharp\sharp A\leq\sharp A$. Now we proceed by structural induction on $A_{Q}$.

• •

$\llparenthesis{\mathsf{qbit}}\rrparenthesis=\sharp\mathbb{B}\simeq\sharp\sharp\mathbb{B}=\sharp\llparenthesis{\mathsf{qbit}}\rrparenthesis$.

• •

$\llparenthesis{A_{Q}\otimes B_{Q}}\rrparenthesis=\sharp(\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis)\simeq\sharp\sharp(\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis)=\sharp\llparenthesis{A_{Q}\otimes B_{Q}}\rrparenthesis$.∎

Theorem VI.5. * Translation preserves typeability:*

If $\Gamma\vdash_{Q}t:A_{Q}$ then $\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis$. 2. 2.

If $\Delta|\Gamma\vdash_{C}t:A$ then $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis$. 3. 3.

If $[Q,L,t]:A$ then $\vdash\llparenthesis{[Q,L,t]}\rrparenthesis:\llparenthesis{A}\rrparenthesis$.

Proof.

Since $\vdash_{Q}$ depends on $\vdash_{C}$, we prove items (1) and (2) at the same time by induction on the typing derivation.

• •

$\Delta,x:A\vdash_{C}x:A$

By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rules (Axiom) and (Weak), we have $\llparenthesis{\Delta}\rrparenthesis,x:\llparenthesis{A}\rrparenthesis\vdash x:\llparenthesis{A}\rrparenthesis$.

• •

$\Delta\vdash_{C}*:\mathbb{U}$

By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rules (Void) and (Weak) we conclude $\llparenthesis{\Delta}\rrparenthesis\vdash*:\mathbb{U}$.

• •

$\Delta\vdash_{C}\lambda x.t:A\to B\Delta,x:A\vdash_{C}t:B$

By the induction hypothesis, ${\llparenthesis{\Delta}\rrparenthesis,x:\llparenthesis{A}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{B}\rrparenthesis}$ and by Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (PureLam), $\llparenthesis{\Delta}\rrparenthesis\vdash\lambda x.\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis\to\llparenthesis{B}\rrparenthesis$.

• •

$\Delta\vdash_{C}tr:B\lx@proof@logical@and\Delta\vdash_{C}t:A\to B\Delta\vdash_{C}r:A$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis\to\llparenthesis{B}\rrparenthesis$ and $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{r}\rrparenthesis:\llparenthesis{A}\rrparenthesis$. Hence, by rules (SubArrows) and (Sub), we have $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis\Rightarrow\llparenthesis{B}\rrparenthesis$, and also, we have $\llparenthesis{\Delta}\rrparenthesis[\sigma]\vdash\llparenthesis{r}\rrparenthesis[\sigma]:\llparenthesis{A}\rrparenthesis$, where $\sigma$ is a substitution of every variable in $\Delta$ by fresh variables. Then, by rule (App) we can derive, $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis[\sigma]\vdash\llparenthesis{t}\rrparenthesis\llparenthesis{r}\rrparenthesis[\sigma]:\llparenthesis{B}\rrparenthesis$. By Lemma VI.2, we have $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (Contr), we get $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis\llparenthesis{r}\rrparenthesis:\llparenthesis{B}\rrparenthesis$.

• •

$\Delta,\Delta\vdash_{C}(t,r):A\times B\lx@proof@logical@and\Delta\vdash_{C}t:A\Delta\vdash_{C}r:B$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A}\rrparenthesis$ and $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{r}\rrparenthesis:\llparenthesis{B}\rrparenthesis$. Hence, by rule (Pair), $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis\vdash(\llparenthesis{t}\rrparenthesis,\llparenthesis{r}\rrparenthesis):\llparenthesis{A}\rrparenthesis\times\llparenthesis{B}\rrparenthesis$.

• •

$\Delta\vdash_{C}\pi_{i}t:A_{i}\Delta\vdash_{C}t:A_{1}\times A_{2}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A_{1}}\rrparenthesis\times\llparenthesis{A_{2}}\rrparenthesis$. By Lemma VI.2, $\llparenthesis{A_{i}}\rrparenthesis\simeq\flat\llparenthesis{A_{i}}\rrparenthesis$ for $i=1,2$, hence, by rules (Axiom) and (Weak), we have $x_{1}:\llparenthesis{A_{1}}\rrparenthesis,x_{2}:\llparenthesis{A_{2}}\rrparenthesis\vdash x_{i}:\llparenthesis{A_{i}}\rrparenthesis$. Therefore, by rule (LetPair), we can derive $\llparenthesis{\Delta}\rrparenthesis\vdash\mathsf{let}\ {(x_{1},x_{2})}={\llparenthesis{t}\rrparenthesis}\ \mathsf{in}\ {x_{i}}:\llparenthesis{A_{i}}\rrparenthesis$.

• •

$\Delta\vdash_{C}\mathtt{t\!t}:\mathsf{bit}$

By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, so, by rules (Void), (InL), and (Weak), we can derive $\llparenthesis{\Delta}\rrparenthesis\vdash\mathtt{t\!t}:\mathbb{B}$.

• •

$\Delta\vdash_{C}\mathtt{f\!f}:\mathsf{bit}$

By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, so, by rules (Void), (InR), and (Weak), we can derive $\llparenthesis{\Delta}\rrparenthesis\vdash\mathtt{f\!f}:\mathbb{B}$.

• •

$\Delta\vdash_{C}\mathtt{i{\mskip-1.0mu}f}~{}t~{}\{r_{1}\mid r_{2}\}:A\lx@proof@logical@and\Delta\vdash_{C}t:\mathsf{bit}\Delta\vdash_{C}r_{1}:A\Delta\vdash_{C}r_{2}:A$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\mathbb{B}=\mathbb{U}+\mathbb{U}$ and for $i=1,2$, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{r_{i}}\rrparenthesis:\llparenthesis{A}\rrparenthesis$. By rules (Axiom) and (Seq), we can derive $\llparenthesis{\Delta}\rrparenthesis,x_{i}:\mathbb{U}\vdash x_{i};\llparenthesis{r_{i}}\rrparenthesis:\llparenthesis{A}\rrparenthesis$ we also have $\llparenthesis{\Delta}\rrparenthesis[\sigma]\vdash\llparenthesis{t}\rrparenthesis[\sigma]:\mathbb{U}+\mathbb{U}$, where $\sigma$ is a substitution of every variable in $\Delta$ by fresh variables. Then, by rule (PureMatch), $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis[\sigma]\vdash\texttt{match}~{}\llparenthesis{t}\rrparenthesis[\sigma]~{}\{\texttt{inl}(x_{1})\mapsto x_{1};\llparenthesis{r}\rrparenthesis~{}|~{}\texttt{inr}(x_{2})\mapsto x_{2};\llparenthesis{s}\rrparenthesis\}:\llparenthesis{A}\rrparenthesis$. By Lemma VI.2, we have $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (Cont), we conclude $\llparenthesis{\Delta}\rrparenthesis\vdash\texttt{match}~{}\llparenthesis{t}\rrparenthesis~{}\{\texttt{inl}(x_{1})\mapsto x_{1};\llparenthesis{r}\rrparenthesis~{}|~{}\texttt{inr}(x_{2})\mapsto x_{2};\llparenthesis{s}\rrparenthesis\}:\llparenthesis{A}\rrparenthesis$

• •

$\Delta|x:A_{Q}\vdash x:A_{Q}$

By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rules (Axiom) and (Weak), we have $\llparenthesis{\Delta}\rrparenthesis,x:\llparenthesis{A}\rrparenthesis\vdash x:\llparenthesis{A}\rrparenthesis$.

• •

$\Delta|\Gamma_{1},\Gamma_{2}\vdash_{Q}s\otimes t:A_{Q}\otimes B_{Q}\lx@proof@logical@and\Delta|\Gamma_{1}\vdash_{Q}s:A_{Q}\Delta|\Gamma_{2}\vdash_{Q}t:B_{Q}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis$ and $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash t:\llparenthesis{B_{Q}}\rrparenthesis$. Then, we can derive $\llparenthesis{\Delta}\rrparenthesis[\sigma],\llparenthesis{\Gamma_{1}}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis[\sigma]:\llparenthesis{A_{Q}}\rrparenthesis$, where $\sigma$ is a substitution on every variable in $\Delta$ by fresh variables. Hence, by rule (Pair), we can derive $\llparenthesis{\Delta}\rrparenthesis[\sigma],\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash(\llparenthesis{s}\rrparenthesis[\sigma],\llparenthesis{t}\rrparenthesis):\llparenthesis{A_{Q}}\rrparenthesis\times\llparenthesis{B_{Q}}\rrparenthesis$. By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (Contr), we have $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash(\llparenthesis{s}\rrparenthesis,\llparenthesis{t}\rrparenthesis):\llparenthesis{A_{Q}}\rrparenthesis\times\llparenthesis{B_{Q}}\rrparenthesis$. Finally, by rules (SharpIntro) and (Sub), we have $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash(\llparenthesis{s}\rrparenthesis,\llparenthesis{t}\rrparenthesis):\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis$.

• •

$\Delta|\Gamma\vdash_{Q}U(t):\mathsf{qbit}\Delta|\Gamma\vdash_{Q}t:\mathsf{qbit}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\sharp\mathbb{B}$. By Proposition IV.11, $\vdash\bar{U}:\sharp\mathbb{B}\to\sharp\mathbb{B}$, hence, by rules (SubArrows) and (Sub), we have $\vdash\bar{U}:\sharp\mathbb{B}\Rightarrow\sharp\mathbb{B}$. Therefore, by rule (App), we can derive $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash\bar{U}\llparenthesis{t}\rrparenthesis:\sharp\mathbb{B}$.

• •

$\Delta|\Gamma_{1},\Gamma_{2}\vdash_{Q}\mathsf{let}\ {x\otimes y}={s}\ \mathsf{in}\ {t}:C_{Q}\lx@proof@logical@and\Delta|\Gamma_{1}\vdash_{Q}s:A_{Q}\otimes B_{Q}\Delta|\Gamma_{2},x:A_{Q},y:B_{Q}\vdash_{Q}t:C_{Q}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis$ and $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis,x:\llparenthesis{A_{Q}}\rrparenthesis,y:\llparenthesis{B_{Q}}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{C_{Q}}\rrparenthesis$. Then, we also have $\llparenthesis{\Delta}\rrparenthesis[\sigma],\llparenthesis{\Gamma_{1}}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis[\sigma]:\llparenthesis{A_{Q}}\rrparenthesis\otimes\llparenthesis{B_{Q}}\rrparenthesis$, where $\sigma$ is a substitution on every variable in $\Delta$ by fresh variables. By Lemma VI.3, $\llparenthesis{A_{Q}}\rrparenthesis\simeq\sharp\llparenthesis{A_{Q}}\rrparenthesis$, $\llparenthesis{B_{Q}}\rrparenthesis\simeq\sharp\llparenthesis{B_{Q}}\rrparenthesis$, and $\llparenthesis{C_{Q}}\rrparenthesis\simeq\sharp\llparenthesis{C_{Q}}\rrparenthesis$. Hence, $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis,x:\sharp\llparenthesis{A_{Q}}\rrparenthesis,y:\sharp\llparenthesis{B_{Q}}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\sharp\llparenthesis{C_{Q}}\rrparenthesis$. Therefore, by rule (LetTens), $\llparenthesis{\Delta}\rrparenthesis[\sigma],\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash\mathsf{let}\ {(x,y)}={\llparenthesis{s}\rrparenthesis[\sigma]}\ \mathsf{in}\ {\llparenthesis{t}\rrparenthesis}:\sharp\llparenthesis{C_{Q}}\rrparenthesis$. By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (Contr), we get $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash\mathsf{let}\ {(x,y)}={\llparenthesis{s}\rrparenthesis}\ \mathsf{in}\ {\llparenthesis{t}\rrparenthesis}:\sharp\llparenthesis{C_{Q}}\rrparenthesis$. Finally, using the fact that $\sharp\llparenthesis{C_{Q}}\rrparenthesis\simeq\llparenthesis{C_{Q}}\rrparenthesis$, we get $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma_{1}}\rrparenthesis,\llparenthesis{\Gamma_{2}}\rrparenthesis\vdash\mathsf{let}\ {(x,y)}={\llparenthesis{s}\rrparenthesis}\ \mathsf{in}\ {\llparenthesis{t}\rrparenthesis}:\llparenthesis{C_{Q}}\rrparenthesis$.

Notice that we have used the following unproved rule: If $\Gamma,x:A\vdash t:B$ and $A\simeq C$, then $\Gamma,x:C\vdash t:B$. Hence, we prove that this rule is true. Assume $\Gamma,x:A\vdash t:B$, then, $t\langle\sigma\rangle\Vdash\llbracket B\rrbracket$ for every $\sigma\in\llbracket\Gamma,x:A\rrbracket=\llbracket\Gamma,x:C\rrbracket$, and so $\Gamma,x:C\vdash t:B$.

• •

$\Delta|\emptyset\vdash_{Q}\mathsf{new}(t):\mathsf{qbit}\Delta\vdash_{C}t:\mathsf{bit}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\mathbb{B}$. We conclude by rules (SharpIntro) and (Sub) that $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\sharp\mathbb{B}$.

• •

$\Delta\vdash_{C}\lambda^{Q}x.t:A_{Q}\multimap B_{Q}\Delta|x:A_{Q}\vdash_{Q}t:B_{Q}$

By the induction hypothesis $\llparenthesis{\Delta}\rrparenthesis,x:\llparenthesis{A_{Q}}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{B_{Q}}\rrparenthesis$. Since $\mathbb{U}\simeq\flat\mathbb{U}$, by rule (Weak), we have $\llparenthesis{\Delta}\rrparenthesis,z:\mathbb{U},x:\llparenthesis{A_{Q}}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{B_{Q}}\rrparenthesis$ Then, by rules (UnitLam) and (PureLam), we can derive $\llparenthesis{\Delta}\rrparenthesis\vdash\lambda zx.\llparenthesis{t}\rrparenthesis:\mathbb{U}\to(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis)$.

• •

$\Delta|\Gamma\vdash_{Q}s@t:B_{Q}\lx@proof@logical@and\Delta\vdash_{C}s:A_{Q}\multimap B_{Q}\Delta|\Gamma\vdash_{Q}t:A_{Q}$

By the induction hypothesis, $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis:\mathbb{U}\to(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis)$ and $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis$. Then, $\llparenthesis{\Delta}\rrparenthesis[\sigma],\llparenthesis{\Gamma}\rrparenthesis\vdash\llparenthesis{t}\rrparenthesis[\sigma]:\llparenthesis{A_{Q}}\rrparenthesis$, where $\sigma$ is a substitution on every variable in $\Delta$ by fresh variables. By rules (SubArrows) and (Sub), we have $\llparenthesis{\Delta}\rrparenthesis\vdash\llparenthesis{s}\rrparenthesis:\mathbb{U}\Rightarrow(\llparenthesis{A_{Q}}\rrparenthesis\Rightarrow\llparenthesis{B_{Q}}\rrparenthesis)$. In addition, by rule (Void), $\vdash*:\mathbb{U}$. Hence, by rule (App) twice, we get $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis,\llparenthesis{\Delta}\rrparenthesis[\sigma]\vdash(\llparenthesis{s}\rrparenthesis*)\llparenthesis{t}\rrparenthesis[\sigma]:\llparenthesis{B_{Q}}\rrparenthesis$. By Lemma VI.2, $\flat\llparenthesis{\Delta}\rrparenthesis\simeq\llparenthesis{\Delta}\rrparenthesis$, hence, by rule (Contr), $\llparenthesis{\Delta}\rrparenthesis,\llparenthesis{\Gamma}\rrparenthesis\vdash(\llparenthesis{s}\rrparenthesis*)\llparenthesis{t}\rrparenthesis:\llparenthesis{B_{Q}}\rrparenthesis$.

Now we prove item (3).

Let

[TABLE]

that means $\emptyset|\textit{FV}(t):\mathsf{qbit}\vdash_{Q}t:A_{Q}$. We must show that

[TABLE]

that is

[TABLE]

From item (1) we have $\textit{FV}(t):\sharp\mathbb{B}\vdash\llparenthesis{t}\rrparenthesis:\llparenthesis{A_{Q}}\rrparenthesis$. Then, by definition, we have $\llparenthesis{t}\rrparenthesis\langle\sigma\rangle\Vdash\llparenthesis{A_{Q}}\rrparenthesis$ for every $\sigma\in\llbracket FV(t):\sharp\mathbb{B}\rrbracket$. In particular, $[\sigma_{i}]=[x_{1}:=\bar{y}_{p(1)}^{i},\dots,x_{n}:=\bar{y}_{p(n)}^{i}]\in\llbracket FV(t):\sharp\mathbb{B}\rrbracket$, so $\llparenthesis{t}\rrparenthesis\langle\sigma_{i}\rangle=\llparenthesis{t}\rrparenthesis[\sigma_{i}]\Vdash\llparenthesis{A_{Q}}\rrparenthesis$. By Lemma VI.3, $\llparenthesis{A_{Q}}\rrparenthesis\simeq\sharp\llparenthesis{A_{Q}}\rrparenthesis$, and so, we have $\sum_{i=1}^{m}\alpha_{i}\cdot\llparenthesis{t}\rrparenthesis[\sigma_{i}]\Vdash\llparenthesis{A_{Q}}\rrparenthesis$, which is, by definition, the same as (1) ∎

Lemma .12**.**

For any terms $t$ and $r$, $\llparenthesis{t[x:=r]}\rrparenthesis=\llparenthesis{t}\rrparenthesis[x:=\llparenthesis{r}\rrparenthesis]$.

Proof.

By a straightforward structural induction on $t$. ∎

Lemma .13**.**

For all value distributions $\vec{v}$ and $\vec{v}$, for all term distributions $\vec{t}$, $\vec{s}$, $\vec{s}_{1}$, $\vec{s}_{2}$ and for all pure values $w$, we have the equalities:

• •

$(\vec{v},\vec{v}^{\prime})[x:=w]=(\vec{v}[x:=w],\vec{v}^{\prime}[x:=w])$**

• •

$\texttt{inl}(\vec{v})[x:=w]=\texttt{inl}(\vec{v}[x:=w])$**

• •

$\texttt{inr}(\vec{v})[x:=w]=Inr{\vec{v}[x:=w]}$**

• •

$(\vec{s}\,\vec{t})[x:=w]=\vec{s}[x:=w]\,\vec{t}[x:=w]$**

• •

$(\vec{t};\vec{s})[x:=w]=\vec{t}[x:=w];\vec{s}[x:=w]$**

• •

$(\texttt{let}~{}(x_{1},x_{2})=\vec{t}~{}\texttt{in}~{}\vec{s})[x:=w]=\texttt{let}~{}(x_{1},x_{2})=\vec{t}[x:=w]~{}\texttt{in}~{}\vec{s}[x:=w]$* (if $x_{1},x_{2}\notin\textit{FV}(w)\cup\{x\}$)*

• •

$(\texttt{match}~{}\vec{t}~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}\})[x:=w]=\texttt{match}~{}\vec{t}[x:=w]~{}\{\texttt{inl}(x_{1})\mapsto\vec{s}_{1}[x:=w]~{}|~{}\texttt{inr}(x_{2})\mapsto\vec{s}_{2}[x:=w]\}$**

Proof.

Let us treat the case of the pair destructing let-construct. Given term distributions $\vec{t}=\sum_{i=1}^{n}\alpha_{i}\cdot{t_{i}}$ and $\vec{s}$, and a pure value $w$ such that $x_{1},x_{2}\notin\textit{FV}(w)\cup\{x\}$, we observe that

[TABLE]

The other cases are treated similarly. ∎

Remark .14** (Parallel substitution).**

The operation of parallel substitution $[x_{1}:=w_{1},\ldots,x_{n}:=w_{n}]$ (where $x_{1},\ldots,x_{n}$ are pairwise distinct variables) can be easily implemented as a sequence of pure substitutions, by temporarily replacing the $x_{i}$’s with fresh names in order to avoid undesirable captures between successive pure substitutions. For instance, we can let

[TABLE]

where $z_{1},\ldots,z_{n}$ are fresh names w.r.t. $\vec{t},x_{1},\ldots,x_{n},w_{1},\ldots,w_{n}$. Note that this precaution is useless when the substituands $w_{1},\ldots,w_{n}$ are closed, since in this case, parallel substitution amounts to the following sequential substitution (whose order is irrelevant):

[TABLE]

Lemma .15**.**

For all term distributions $\vec{t}$ and for all closed value distributions $\vec{v}$ and $\vec{w}$:

[TABLE]

Theorem VI.6 (Adequacy). If $[Q,L,t]\to[Q^{\prime},L^{\prime},r]$, then $\llparenthesis{[Q,L,t]}\rrparenthesis\mathrel{{\succ}\mskip-6.0mu{\succ}}\llparenthesis{[Q^{\prime},L^{\prime},r]}\rrparenthesis$.

Proof.

We proceed by induction on the rewrite relation of $\lambda_{Q}$. We only give the cases where $C(\cdot)=\{\cdot\}$, as other cases are simple calls to the induction hypothesis. In all the cases, we consider $Q=\sum_{i=1}^{m}\alpha_{i}|u_{1}^{i},\dots,y_{n}^{i}\rangle$, $L=\{x_{1}:=p(1),\dots,x_{n}:=p(n)\}$, and $[\sigma_{i}]=[x_{1}:=\bar{y}_{p(1)}^{i},\dots,x_{n}:=\bar{y}_{p(n)}^{i}]$.

• •

$[Q,L,(\lambda x.t)u]\to[Q,L,t[x:=u]]$.

[TABLE]

• •

$[Q,L,(\lambda^{Q}x.t)@u]\to[Q,L,t[x:=u]]$.

[TABLE]

• •

$[Q,L,\pi_{1}(u,v)]\to[Q,L,u]$.

[TABLE]

• •

$[Q,L,\pi_{s}(u,v)]\to[Q,L,v]$.

[TABLE]

• •

$[Q,L,\mathtt{i{\mskip-1.0mu}f}~{}\mathtt{t\!t}~{}\{t\mid r\}]\to[Q,L,t]$

[TABLE]

• •

$[Q,L,\mathtt{i{\mskip-1.0mu}f}~{}\mathtt{f\!f}~{}\{t\mid r\}]\to[Q,L,r]$

[TABLE]

• •

$[Q,L,\mathsf{let}\ {x\otimes y}={t\otimes r}\ \mathsf{in}\ {s}]\to[Q,L,s[x:=t,y:=r]]$.

[TABLE]

• •

$[\emptyset,\emptyset,\mathsf{new}(\mathtt{t\!t})]\to[|1\rangle,\{x\mapsto 1\},x]$

[TABLE]

• •

$[\emptyset,\emptyset,\mathsf{new}(\mathtt{f\!f})]\to[|0\rangle,\{x\mapsto 1\},x]$

[TABLE]

• •

$[|\psi\rangle,\{x\mapsto 1\},U(x)]\to[U|\psi\rangle,\{x\mapsto 1\},x]$.

Let $U|0\rangle=\gamma_{0}|0\rangle+\delta_{0}|1\rangle$ and $U|1\rangle=\gamma_{1}|0\rangle+\delta_{1}|1\rangle$. Then,

[TABLE]