一句话：构造 DiLL 的经典指称语义模型，基于核拓扑向量空间与紧支分布，使证明的线性近似对应通常微分。
Differential Linear Logic（DiLL）在 linear logic 上增加了证明的线性近似概念。DiLL 是经典逻辑，具有对合否定，但此前缺少经典指称模型能使其中的微分对应光滑函数上的通常微分。该文构造了基于核拓扑向量空间与紧支分布的模型，从而为 DiLL 提供了这样一个经典指称语义，使证明的线性近似与分布意义下的微分一致。该工作为线性偏微分方程提供了逻辑与语义基础。
Differential Linear Logic (DiLL), introduced by Ehrhard and Regnier, extends linear logic with a notion of linear approximation of proofs. While DiLL is classical logic, i.e. has an involutive negation, classical denotational models of it in which this notion of differentiation corresponds to the usual one, defined on any smooth function, were missing. We solve this issue by constructing a model of it based on nuclear topological vector spaces and distributions with compact support.
DOI 原文 ·
@inproceedings{paperbot4319,
title = {A Logical Account for Linear Partial Differential Equations},
author = {Marie Kerjean},
booktitle = {LICS},
year = {2018},
doi = {10.1145/3209108.3209192}
}