用范畴论方法实现直觉逻辑与函数程序的同态加密，支持安全计算。
Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
- 基于多项式函子和有界自然函子构建逻辑与程序的代数结构
- 提出BNF区分问题作为密码安全性基础，归约自子图同构问题
- 可对依赖类型函数程序进行同态执行，适合隐私保护计算场景
我们提出一个概念框架，将同态加密从算术或布尔运算扩展到直觉逻辑证明领域，并通过柯里-霍华德对应关系延伸至类型化函数程序。首先回顾算术同态加密方案，随后讨论如何将类似思想应用于直觉逻辑中的推理步骤。核心构造依赖于多项式函子和有界自然函子（BNFs），它们构成逻辑公式与证明表示与操作的范畴基础。我们提出了一个复杂性理论上的安全假设——BNF区分问题，通过从子图同构问题的归约建立其安全性基础。最后，描述了该方法如何同态编码总函数、依赖类型函数程序的执行过程，并提出软件优化与硬件加速策略以提升实际效率。
原文摘要 · Abstract (English)
We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional programs. We begin by reviewing well-known homomorphic encryption schemes for arithmetic operations, and then discuss the adaptation of similar concepts to support logical inference steps in intuitionistic logic. Key to our construction are polynomial functors and Bounded Natural Functors (BNFs), which serve as a categorical substrate on which logic formulas and proofs are represented and manipulated. We outline a complexity-theoretic hardness assumption -- the BNF Distinguishing Problem, constructed via a reduction from Subgraph Isomorphism, providing a foundation for cryptographic security. Finally, we describe how these methods can homomorphically encode the execution of total, dependently typed functional programs, and outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。