直觉逻辑证明与函数式程序的同态加密：受合数阶双线性群启发的范畴论方法
计算机科学中的逻辑
2025-03-11 v1 人工智能
摘要
我们提出了一个概念框架，将同态加密从算术或布尔运算扩展到直觉逻辑证明领域，并根据 Curry-Howard 对应扩展到类型化函数式程序领域。我们首先回顾了用于算术运算的已知同态加密方案，然后讨论了如何将类似概念进行改造以支持直觉逻辑中的逻辑推理步骤。我们构建的关键在于多项式函子与有界自然函子，它们作为范畴论基底，在其上表示并操作逻辑公式与证明。我们概述了一个复杂度理论上的困难假设——BNF 区分问题，该问题通过从子图同构问题归约构建，为密码学安全性提供了基础。最后，我们描述了这些方法如何对完全的、依赖类型函数式程序的执行进行同态编码，并概述了使该方法具备潜在效率的策略，包括软件优化与硬件加速。
引用
@article{arxiv.2503.05779,
title = {Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups},
author = {Ben Goertzel},
journal= {arXiv preprint arXiv:2503.05779},
year = {2025}
}