Metric λ‑calculus with conditionals: quantum, probabilities and beyond

Abstract

In recent decades, there has been an effort in computer science to move beyond rigid binary notions—such as equality and bisimulation—toward more flexible approaches that better reflect the subtleties of real‑world computation. Traditional program equivalence, for example, is purely dichotomous: two programs are either equivalent or not. Yet in many computational paradigms, this binary perspective proves too restrictive. For instance, in contexts involving physical environments and noisy data, more nuanced notions — such as approximate program equivalence—emerge naturally. It is within this evolving landscape that our work is situated. Specifically, we build on the work of [36], which introduced a quantalic equational deductive system for the linear ‑calculus, along with a proof of its soundness and completeness. We extend their framework by introducing a metric equation for conditionals and proving its soundness and completeness. Syntactically, to illustrate the utility of this metric equation, we present a metric version of copairing’s extensionality. On the semantic side, we present five categories that satisfy the necessary requirements for interpreting this equation, thereby demonstrating the broad applicability of our approach across several domains. Finally, we illustrate the use of the metric equation in more detail within both the probabilistic and quantum computing paradigms. For quantum models, we focus on the first‑order fragment of the λ‑calculus, though extensions to higher‑order are possible using advanced categorical tools, as in [36].

Nas últimas décadas, em ciência da computação, tem‑se assistido a um esforço no sentido de nos libertarmos das rígidas amarras binárias associadas a noções como igualdade e bisimulação, explorando abordagens mais flexíveis que captem melhor as subtilezas da computação no mundo real. Por exemplo, a noção tradicional de equivalência de programas é puramente dicotómica: dois programas ou são equivalentes, ou não o são. No entanto, em muitos paradigmas computacionais, esta perspetiva binária revela‑se demasiado restritiva. Em contextos que envolvem interação com o meio ou dados ruidosos, surgem naturalmente noções mais subtis, como a equivalência aproximada de programas. É precisamente neste enquadramento que se insere a presente dissertação, ao estender o trabalho de [36], no qual foi introduzido um sistema equacional quantálico para o cálculo‑λ, juntamente com as respetivas provas de correção e completude. Mais concretamente, neste trabalho propomos uma equação métrica para condicionais e demonstramos a sua correção e completude. Do ponto de vista sintático, para ilustrar a utilidade desta equação métrica, apresentamos uma versão métrica da extensionalidade do copairing. Do ponto de vista semântico, identificamos cinco categorias que satisfazem os requisitos necessários para interpretar esta equação, demonstrando assim a ampla aplicabilidade da nossa abordagem em vários domínios. Por fim, ilustramos com mais detalhe a utilização da equação métrica nos paradigmas de computação probabilística e quântica. No caso dos modelos quânticos, focamo‑nos no fragmento de primeira ordem do cálculo‑λ , embora sejam possíveis extensões para ordem superior através de ferramentas categóricas mais avançadas, assim como em [36].