avatar_hypergraph_rewriting

Crates.ioavatar_hypergraph_rewriting
lib.rsavatar_hypergraph_rewriting
version0.1.1
sourcesrc
created_at2021-11-13 22:25:40.192821
updated_at2021-11-14 07:43:43.925901
descriptionHypergraph rewriting system with avatars for symbolic distinction
homepagehttps://github.com/advancedresearch/avatar_hypergraph_rewriting
repositoryhttps://github.com/advancedresearch/avatar_hypergraph_rewriting.git
max_upload_size
id481551
size33,362
Sven Nilsen (bvssvni)

documentation

README

Avatar Hypergraph Rewriting

Hypergraph rewriting system with avatars for symbolic distinction

Based on paper Avatar Hypergraph Rewriting.

Avatars can be used on the left side of rewriting rules to control symbolic distinction of nodes in the hypergraph evolution. They can be used on any hyperedge.

Example: Wolfram vs Avatar

use avatar_hypergraph_rewriting::*;

use Expr::*;

fn main() {
    // `{0,0}`
   let a = vec![Nat(0), Nat(0)];

    // `{1,2} -> {}`
    let wolfram_rule = Rule(vec![Nat(1), Nat(2)], vec![]);
    // prints `{}` because `{0,0}` is reduced.
    println!("{}", format(&wolfram_rule.parallel(&a)));

    // `{a'(1),b'(2)} -> {}`
    let avatar_rule = Rule(vec![ava("a", 1), ava("b", 2)], vec![]);
    // prints `{0,0}` because avatars "a" and "b" must be different nodes.
    println!("{}", format(&avatar_rule.parallel(&a)));
}

Motivation

Avatar Hypergraph Rewriting (AHR) is an attempt to find an Avatar Extension of Wolfram models that satisfies the assumptions in the paper Consciousness in Wolfram Models.

Wolfram models are used in the Wolfram Physics Project, which seeks to explain fundamental physics using a hypergraph rewriting system.

Wolfram models correspond to theorem proving with Intuitionistic Propositional Logic (IPL), which can be generalised to Homotopy Type Theory. For more information, see this paper by Xerxes D. Arsiwalla and Jonathan Gorard.

IPL is the foundation for Type Theory and modern mathematical foundations. IPL is weaker than Propositional Logic (PL).

  • PL is called "classical" logic and satisfies a Boolean algebra
  • IPL is called "constructive" logic and satisfies a Heyting algebra

However, in Path Semantics there is an even weaker logic called Path Semantical Intuitionistic Propositional Logic (PSI).

PSI is much less understood than IPL and PL, but is relevant for the philosophy of mathematical language design. One thing that makes PSI different from IPL is that a quality operator ~~ lifts biconditions with symbolic distinction (quality is a partial equivalence).

A closely related research topic to PSI is Avatar Extensions.

This hypergraph rewriting system combines the property of symbolic distinction with avatars. The avatars is a design choice to express symbolic distinction efficiently.

Commit count: 9

cargo fmt