New rough draft, work in progress, subject to revisions etc.
https://wiki.opencog.org/w/File:A_Formalization_of_Hyperon_MeTTa_language_in_terms_of_metagraph_rewriting.pdf
Latest notions of theory behind "Atomese 2" aka MeTTa basically... a
small piece of the ongoing work toward OpenCog Hyperon version...
ben
\begin{abstract}
MeTTa (Meta Type Talk) is a novel programming language created for use
in the OpenCog Hyperon AGI system. It is designed as a meta-language
with very basic and general facilities for handling symbols,
groundings, variables, types, substitutions and pattern matching.
Primitives exist for creating new type systems and associated DSLs,
the intention being that most MeTTa programming takes place within
such DSLs.
Informally, MeTTa is Hyperon's lowest-level "language of thought" --
the meta-language in which algorithms for learning more particular
knowledge representations, will operate, and in which these algorithms
themselves may be represented. Tractable representation of a variety
of knowledge and cognitive process types in this sort of formalism has
been explored in a long history of publications and software systems.
Here we explain how one might go about formalizing the MeTTa language
as a system of metagraph rewrite rules, an approach that fits in
naturally to the Hyperon framework given that the latter's core
component is a distributed metagraph knowledge store (the Atomspace).
The metagraph rewrite rules constituting MeTTa programs can also be
represented as metagraphs, giving a natural model for MeTTa reflection
and self-modifying code.
Considering MeTTa programs that compute equivalences between execution
traces of other MeTTa programs allows us to model spaces of MeTTa
execution traces using Homotopy Type Theory. Considering the limit
of MeTTa programs mapping between execution traces of MeTTa programs
that map between execution traces of MeTTa programs that $\ldots$, we
find that a given MeTTa codebase is effectively modeled as an
$\infty-\textrm{groupoid}$, and the space of all MeTTa codebases as an
$(\infty, 1)-\textrm{topos}$. This topos is basically the same as the
so-called "Ruliad" previously derived from rewrite rules on
hypergraphs, in a discrete physics context.
The formalization of MeTTA as metagraph rewrite rules may also provide
a useful framework for structuring the implementation of efficient
methods for pattern matching and equality inference within the MeTTa
interpreter.
\end{abstract}
--
Ben Goertzel, PhD
[email protected]
"My humanity is a constant self-overcoming" -- Friedrich Nietzsche
------------------------------------------
Artificial General Intelligence List: AGI
Permalink:
https://agi.topicbox.com/groups/agi/T0d365b953350e4ce-M9cc582743839efdc9ddea7cb
Delivery options: https://agi.topicbox.com/groups/agi/subscription
