paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Realizability in the Unitary Sphere

酉球中的可实现性
LICS 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2019匹配度 3/10 · 论文研究线性代数 λ-演算的可实现性语义与酉性类型规则，属于量子编程语言形式语义；与用户核心方向（静态分析、LLM/Agent 改进静态分析、浮点/贝叶斯程序分析及其与 LLM 交叉）无直接关联。虽然形式语义符合用户对理论形式化的偏好，但缺乏静态分析、LLM/Agent 或工业落地元素，量子主题也未被用户画像明确覆盖。引用 13 inbox
Alejandro Diaz-Caro, Mauricio Guillermo, Alexandre Miquel, Benoit Valiron
形式语义量子与概率编程
crossref: 2026-09-12

AI 速览

一句话：提出基于可实现性的线性代数 λ-演算语义，刻画酉性并导出类型规则，可扩展至经典与量子 λ-演算。

本文研究线性代数 λ-演算中长期缺乏的酉性（unitarity）语义刻画问题。作者提出一种基于可实现性（realizability）的语义，将系统项解释到酉球上，从而给出酉性的语义定义，回答了该领域的一个长期问题。基于该语义，作者导出了一套简单类型线性代数 λ-演算的定型规则，并说明该语义与类型系统如何扩展到经典 λ-演算和量子 λ-演算。该工作为线性代数与量子计算中的 λ-演算提供了统一的语义与类型论基础。

问题
如何为线性代数 λ-演算给出酉性的语义刻画，并为其提供类型规则。
方法
基于可实现性构造语义，将项解释到酉球上，并从语义导出简单类型线性代数 λ-演算的定型规则。
评估
以理论构造为主：通过推导类型规则，并展示该语义可扩展至经典与量子 λ-演算来论证其适用性。
原文摘要（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.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot5026,
  title = {Realizability in the Unitary Sphere},
  author = {Alejandro Diaz-Caro and Mauricio Guillermo and Alexandre Miquel and Benoit Valiron},
  booktitle = {LICS},
  year = {2019},
  doi = {10.1109/lics.2019.8785834}
}