Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups

• URL: http://arxiv.org/abs/2503.05779v1
• Date: Wed, 26 Feb 2025 10:10:10 GMT
• Title: Homomorphic Encryption of Intuitionistic Logic Proofs and Functional Programs: A Categorical Approach Inspired by Composite-Order Bilinear Groups
• Authors: Ben Goertzel,
• Abstract summary: We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic.<n>We outline strategies for making the approach potentially efficient, including software optimizations and hardware acceleration.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• MST3 Encryption improvement with three-parameter group of Hermitian function field [0.0]
  This work presents an advanced cryptographic framework utilizing automorphism groups as the foundational structure for encryption scheme implementation. A key innovation in this implementation is utilizing the Hermitian function field as the underlying mathematical framework. The encryption mechanism features phased key de-encapsulation from ciphertext, representing a substantial advantage over alternative implementations.
  arXiv  Detail & Related papers  (2025-04-21T18:58:42Z)
• On Computational Indistinguishability and Logical Relations [1.024113475677323]
  The work concludes with the presentation of an example of a security proof in which the encryption scheme induced by a pseudorandom function is proven secure against active adversaries in a purely equational style.
  arXiv  Detail & Related papers  (2024-08-30T15:08:51Z)
• An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
  This approach allows for the computer-assisted analysis of abstract dialectical frameworks. Exemplary applications include the formal analysis and verification of meta-theoretical properties.
  arXiv  Detail & Related papers  (2023-12-08T09:32:26Z)
• Query Structure Modeling for Inductive Logical Reasoning Over Knowledge Graphs [67.043747188954]
  We propose a structure-modeled textual encoding framework for inductive logical reasoning over KGs. It encodes linearized query structures and entities using pre-trained language models to find answers. We conduct experiments on two inductive logical reasoning datasets and three transductive datasets.
  arXiv  Detail & Related papers  (2023-05-23T01:25:29Z)
• The Predictive Forward-Forward Algorithm [79.07468367923619]
  We propose the predictive forward-forward (PFF) algorithm for conducting credit assignment in neural systems. We design a novel, dynamic recurrent neural system that learns a directed generative circuit jointly and simultaneously with a representation circuit. PFF efficiently learns to propagate learning signals and updates synapses with forward passes only.
  arXiv  Detail & Related papers  (2023-01-04T05:34:48Z)
• Object Representations as Fixed Points: Training Iterative Refinement Algorithms with Implicit Differentiation [88.14365009076907]
  Iterative refinement is a useful paradigm for representation learning. We develop an implicit differentiation approach that improves the stability and tractability of training.
  arXiv  Detail & Related papers  (2022-07-02T10:00:35Z)
• A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
  We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools.
  arXiv  Detail & Related papers  (2021-10-18T10:45:59Z)
• Refining Labelled Systems for Modal and Constructive Logics with Applications [0.0]
  This thesis serves as a means of transforming the semantics of a modal and/or constructive logic into an 'economical' proof system. The refinement method connects two proof-theoretic paradigms: labelled and nested sequent calculi. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics.
  arXiv  Detail & Related papers  (2021-07-30T08:27:15Z)
• Dynamic programming by polymorphic semiring algebraic shortcut fusion [1.9405875431318445]
  Dynamic programming (DP) is an algorithmic design paradigm for the efficient, exact solution of intractable, problems. This paper presents a rigorous algebraic formalism for systematically deriving DP algorithms, based on semiring.
  arXiv  Detail & Related papers  (2021-07-05T00:51:02Z)
• Fractal Structure and Generalization Properties of Stochastic Optimization Algorithms [71.62575565990502]
  We prove that the generalization error of an optimization algorithm can be bounded on the complexity' of the fractal structure that underlies its generalization measure. We further specialize our results to specific problems (e.g., linear/logistic regression, one hidden/layered neural networks) and algorithms.
  arXiv  Detail & Related papers  (2021-06-09T08:05:36Z)
• Differentiable Inductive Logic Programming for Structured Examples [6.8774606688738995]
  We propose a new framework to learn logic programs from noisy and structured examples. We show that our new framework can learn logic programs from noisy and structured examples, such as sequences or trees. Our framework can be scaled to deal with complex programs that consist of several clauses with function symbols.
  arXiv  Detail & Related papers  (2021-03-02T13:47:33Z)
• Patterns of Cognition: Cognitive Algorithms as Galois Connections Fulfilled by Chronomorphisms On Probabilistically Typed Metagraphs [0.0]
  It is argued that a broad class of AGI-relevant algorithms can be expressed in a common formal framework. Examples are drawn from the core cognitive algorithms used in the OpenCog AGI framework.
  arXiv  Detail & Related papers  (2021-02-21T10:50:40Z)
• Finite-Function-Encoding Quantum States [52.77024349608834]
  We introduce finite-function-encoding (FFE) states which encode arbitrary $d$-valued logic functions. We investigate some of their structural properties.
  arXiv  Detail & Related papers  (2020-12-01T13:53:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.