-
OpenCog Hyperon: A Framework for AGI at the Human Level and Beyond
Authors:
Ben Goertzel,
Vitaly Bogdanov,
Michael Duncan,
Deborah Duong,
Zarathustra Goertzel,
Jan Horlings,
Matthew Ikle',
Lucius Greg Meredith,
Alexey Potapov,
Andre' Luiz de Senna,
Hedra Seid Andres Suarez,
Adam Vandervorst,
Robert Werko
Abstract:
An introduction to the OpenCog Hyperon framework for Artificiai General Intelligence is presented. Hyperon is a new, mostly from-the-ground-up rewrite/redesign of the OpenCog AGI framework, based on similar conceptual and cognitive principles to the previous OpenCog version, but incorporating a variety of new ideas at the mathematical, software architecture and AI-algorithm level. This review ligh…
▽ More
An introduction to the OpenCog Hyperon framework for Artificiai General Intelligence is presented. Hyperon is a new, mostly from-the-ground-up rewrite/redesign of the OpenCog AGI framework, based on similar conceptual and cognitive principles to the previous OpenCog version, but incorporating a variety of new ideas at the mathematical, software architecture and AI-algorithm level. This review lightly summarizes: 1) some of the history behind OpenCog and Hyperon, 2) the core structures and processes underlying Hyperon as a software system, 3) the integration of this software system with the SingularityNET ecosystem's decentralized infrastructure, 4) the cognitive model(s) being experimentally pursued within Hyperon on the hopeful path to advanced AGI, 5) the prospects seen for advanced aspects like reflective self-modification and self-improvement of the codebase, 6) the tentative development roadmap and various challenges expected to be faced, 7) the thinking of the Hyperon team regarding how to guide this sort of work in a beneficial direction ... and gives links and references for readers who wish to delve further into any of these aspects.
△ Less
Submitted 19 September, 2023;
originally announced October 2023.
-
Meta-MeTTa: an operational semantics for MeTTa
Authors:
Lucius Gregory Meredith,
Ben Goertzel,
Jonathan Warrell,
Adam Vandervorst
Abstract:
We present an operational semantics for the language MeTTa.
We present an operational semantics for the language MeTTa.
△ Less
Submitted 26 May, 2023;
originally announced May 2023.
-
Representing operational semantics with enriched Lawvere theories
Authors:
Michael Stay,
L. G. Meredith
Abstract:
Many term calculi, like lambda calculus or pi calculus, involve binders for names, and the mathematics of bound variable names is subtle. Schoenfinkel introduced the SKI combinator calculus in 1924 to clarify the role of quantified variables in intuitionistic logic by eliminating them. Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculu…
▽ More
Many term calculi, like lambda calculus or pi calculus, involve binders for names, and the mathematics of bound variable names is subtle. Schoenfinkel introduced the SKI combinator calculus in 1924 to clarify the role of quantified variables in intuitionistic logic by eliminating them. Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculus, but her combinators still depend on the new operator to bind names. Recently, Meredith and Stay showed how to modify Yoshida's combinators by replacing new and replication with reflective operators to provide the first combinator calculus with no bound names into which the asynchronous pi calculus has a faithful embedding. Here we provide an alternative set of combinators built from SKI plus reflection that also eliminates all nominal phenomena, yet provides a faithful embedding of a reflective higher-order pi calculus. We show that with the nominal features effectively eliminated as syntactic sugar, multisorted Lawvere theories enriched over graphs suffice to capture the operational semantics of the calculus.
△ Less
Submitted 10 April, 2017;
originally announced April 2017.
-
Name-free combinators for concurrency
Authors:
Lucius Gregory Meredith,
Michael Stay
Abstract:
Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculus, but her combinators still depend on the "new" operator to bind names. We modify Yoshida's combinators by replacing "new" and replication with reflective operators to provide the first combinator calculus with no bound names into which the asynchronous pi calculus has a faithful embed…
▽ More
Yoshida demonstrated how to eliminate the bound names coming from the input prefix in the asynchronous pi calculus, but her combinators still depend on the "new" operator to bind names. We modify Yoshida's combinators by replacing "new" and replication with reflective operators to provide the first combinator calculus with no bound names into which the asynchronous pi calculus has a faithful embedding. We also show that multisorted Lawvere theories enriched over graphs suffice to capture the operational semantics of the calculus.
△ Less
Submitted 18 April, 2019; v1 submitted 21 March, 2017;
originally announced March 2017.
-
Logic as a distributive law
Authors:
Mike Stay,
Lucius Gregory Meredith
Abstract:
We present an algorithm for deriving a spatial-behavioral type system from a formal presentation of a computational calculus. Given a 2-monad Calc: Catv$\to$ Cat for the free calculus on a category of terms and rewrites and a 2-monad BoolAlg for the free Boolean algebra on a category, we get a 2-monad Form = BoolAlg + Calc for the free category of formulae and proofs. We also get the 2-monad BoolA…
▽ More
We present an algorithm for deriving a spatial-behavioral type system from a formal presentation of a computational calculus. Given a 2-monad Calc: Catv$\to$ Cat for the free calculus on a category of terms and rewrites and a 2-monad BoolAlg for the free Boolean algebra on a category, we get a 2-monad Form = BoolAlg + Calc for the free category of formulae and proofs. We also get the 2-monad BoolAlg $\circ$ Calc for subsets of terms. The interpretation of formulae is a natural transformation $\interp{-}$: Form $\Rightarrow$ BoolAlg $\circ$ Calc defined by the units and multiplications of the monads and a distributive law transformation $δ$: Calc $\circ$ BoolAlg $\Rightarrow$ BoolAlg $\circ$ Calc. This interpretation is consistent both with the Curry-Howard isomorphism and with realizability. We give an implementation of the "possibly" modal operator parametrized by a two-hole term context and show that, surprisingly, the arrow type constructor in the $λ$-calculus is a specific case. We also exhibit nontrivial formulae encoding confinement and liveness properties for a reflective higher-order variant of the $π$-calculus.
△ Less
Submitted 16 October, 2016; v1 submitted 7 October, 2016;
originally announced October 2016.
-
Linear Types Can Change the Blockchain
Authors:
Lucius Gregory Meredith
Abstract:
We give an interpretation of full classical linear logic, and linear proofs in terms of operations on the blockchain.
We give an interpretation of full classical linear logic, and linear proofs in terms of operations on the blockchain.
△ Less
Submitted 2 June, 2015;
originally announced June 2015.
-
Higher category models of the pi-calculus
Authors:
Mike Stay,
Lucius Gregory Meredith
Abstract:
We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an explicit interpretation of the rewrite rules of standard operational presentations as 2-morphisms. One of the key co…
▽ More
We present an approach to modeling computational calculi using higher category theory. Specifically we present a fully abstract semantics for the pi-calculus. The interpretation is consistent with Curry-Howard, interpreting terms as typed morphisms, while simultaneously providing an explicit interpretation of the rewrite rules of standard operational presentations as 2-morphisms. One of the key contributions, inspired by catalysis in chemical reactions, is a method of restricting the application of 2-morphisms interpreting rewrites to specific contexts.
△ Less
Submitted 22 September, 2015; v1 submitted 16 April, 2015;
originally announced April 2015.
-
Policy as Types
Authors:
Lucius G Meredith,
Mike Stay,
Sophia Drossopoulou
Abstract:
Drossopoulou and Noble argue persuasively for the need for a means to express policy in object-capability-based systems. We investigate a practical means to realize their aim via the Curry-Howard isomorphism. Specifically, we investigate representing policy as types in a behavioral type system for the RHO-calculus, a reflective higher-order variant of the pi-calculus.
Drossopoulou and Noble argue persuasively for the need for a means to express policy in object-capability-based systems. We investigate a practical means to realize their aim via the Curry-Howard isomorphism. Specifically, we investigate representing policy as types in a behavioral type system for the RHO-calculus, a reflective higher-order variant of the pi-calculus.
△ Less
Submitted 30 July, 2013; v1 submitted 29 July, 2013;
originally announced July 2013.
-
Knots as processes: a new kind of invariant
Authors:
L. G. Meredith,
David F. Snyder
Abstract:
We exhibit an encoding of knots into processes in the π-calculus such that knots are ambient isotopic if and only their encodings are weakly bisimilar.
We exhibit an encoding of knots into processes in the π-calculus such that knots are ambient isotopic if and only their encodings are weakly bisimilar.
△ Less
Submitted 10 September, 2010;
originally announced September 2010.
