Project - Indexing existing Abstract Models (2024-2025?)

[FadiShawki]

Project - Indexing existing Abstract Models (2024-2025?)

Once a proper interface for Rays is setup, one of the things I'd like to do with it, is to point it to a lot of existing abstract models of computation/mathematics/calculi/theorem-provers/compilers/proof assistants/automated program synthesizers/.../programming languages. And create a way of analyzing/comparing them which does not include manual human labor of specifying their grammars.

• Rays are probably a Characteristica_universalis (Or rather a Universal Language, or as [[Jonathan Gorard]] phrased a similar concept; a "general theory of graphs" (See [[Category Theory]] notes when at [[Society for Multidisciplinary and Fundamental Research (SEMF)]]))

• [[Society for Multidisciplinary and Fundamental Research (SEMF)]] discord equivalent: https://discord.com/channels/844566471501414463/1225907185079287971

---

Comments on [[2024-04-05]]

This thing is probably way too big a project, but thinking about it will probably get much easier in the coming years. I'm preemptively putting this here mainly because I want to find out if there are currently (or have been) people attempting something like this.

The only stuff I've been able to find so far is either incredibly limited in scope or is doing too much of this by hand. Would love to find out that there's someone who has been working on this already though :upside_down:

Seamless direct (partial) inter-compilation/.../translation of things will probably become much more tractable at some point in the near future ^ Though all the more insane complexity of software/firmware/hardware to me seem to pose the most challenges.

---

• [ ] This entire thing should be compiled into a writing/study of existing stuff

---

• [ ] Whole project makes it necessary to get the practical low-level systems in this too.
  • [ ] Lookup existing projects in that space, decompilers, interfaces for binary analysis etc..

---

This is a current list of the projects I found so far related to this project - and possibly some to apply the beast to:

• Chyp, Coq, Agda, LLVM, Unicode, nLab, Category Theory, WebAssembly, WebAssembly System Interface, Wasm SpecTec, OCaml, Backus-Naur Form (BNF), UniMath, Lean, Type Theory, Set Theory, Metamath, Mizar System, NuPRL, HOL, Homotopy Type Theory, Dependent Type Theory, Hopf algebdra, Prover9, Otter, Z3, CUDA, x86, HVM, HOL, Kind, Haskell, WebGPU, Treesitter, MathJax, Gen.jl, Julia, Idris, Quantomatic, Interaction nets, Petri net, Lie algebra, Rzk, cubicaltt, SageMath, Xena Project, Formal Abstract (FAbstracts), Dedukti, TPTP, Isabelle, Nekoka, E (Theorem Prover), SPASS, CVC, Wolfram Language, MiniSat, PicoSAT , microsat, SPUR, miniC2D, clasp, sat-research, Project Everest, pyfolderol, Research in Software Engineering (RiSE), LFSC Checker, nunchaku, CaDiCaL, Boolector, ddSMT, Bitwuzla, Quantumcodes.io, pl-catalog, Group Explorer, lambda-calculus-visualizations, Cohomology, yatima, Paper-Proof
• switchboard, Why3, pyzx, homotopy.io, The Incredible Proof Machine, formal-proofs, Formal Verification, Leo, ProofNet Isabelle, Unilab, MetiTarski, eo, Clojure, Glencoe, aeneas, GAPT, coch-demo, NQTHM, ACL2, LEGO, ALF, Twelf, [Epigram](https://en.wikipedia.org/wiki/Epigram_(programming_language), Saturn, ProvingGround, Elm, Lua, Qt, Bazel, Docker, pp, GrapeVine, HOL Light, itex2MML, reStructuredText, Cyc, Combinators, IPFS, IPLD, Pandoc, LaTeX, dolmen, Andromeda, QED,
• Spectral graph theory, Python: wolfram_model, SetReplace, hypercore-decomposition, higher-order-motifs, XGI, hypergraphx, Probabilistic programming, BoomFilters, MJr, Agents.jl, particle-life, Lenia, The-Powder-Toy, Procedural generation,
• [ ] https://en.wikipedia.org/wiki/Probabilistic_programming
  • [ ] Analytica, bayesloop, Bean Machine, CuPPL, Venture, Probabilistic-C, Anglican, IBAL, BayesDB, PRISM, Infer.NET, dimple, chimple, BLOG, diff-SAT, PSQL, BUGS, FACTORIE, PMTK, Alchemy, Dyna, Figaro, Church, ProbLog, ProBT, Stan, Hakaru, BAli-Phy, ProbCog, Gamble, PWhile, Tuffy, PyMC, Rainier, greta, pomegranate, Lea, WebPPL, Let's Chance, Picture, Turing.jl, Low-level First-order PPL, Troll, Edward, TensorFlow Probability, Edward2, Pyro, NumPyro, Saul, RankPL, Birch, PSI, Blang, MultiVerse
• [Erlang](https://en.wikipedia.org/wiki/Erlang_(programming_language), metalang99, SL, Abstract object theory (AOT), Causal graph, chemlambda, Representation theory, Lattice theory, Metamathematics, archon
• Solid,
• Chemistry: Assembly Theory
• liquidsoap, The Munich Quantum Toolkit (MQT),
• https://github.com/StructuralXplorationLab/Libra (Parametric Design)

Some other names I found but didn't save a link to:

• DisCoPy2, Aletha, Inkresat, F star, smt-comp, starexec, verdict, vau calculus, SF-Calculus, Monoidal Computer, Certora Prover, smt workshop, Imandra, Waldmeister, POG, QuiZX, Globular, proofweb, holyhammer, B, Event-B, TLA+, Atelier B, Rodin, TLAPS, OpenTheory, FoCaLize, Zenon, iProver, CoqinE, veriT, BWare, B-Method, ArchSAT, sel4, HOL4, Flexiformalized math, OMDoc, Schurr 1999, GP/GP2 Plump 2009, GRAPE / Grape PRess - Weber 2017/2021, AGG Taentzer 2004, FUJABA Nickel 2000, GReAT Agrawal 2006, GROOVE Rensik 2004, TPS, PhoX, Markdown, JPEG, JPG, PNG, MINLOG, Jape, ae (alt-ergo), dimacs, iCNF, smtlib, zf (zipperposition), HELM, MathWeb, MathScheme, MathClasses, ForMath Project, Opetopic Type Theory, RedPRL, yaccyt, redtt, PVS, Matita, Guru, Dependent ML, Gallina, Cayenne, Arend
• Ro, aUI

Some Interface design / ... / visualization / game / generation projects

• Unit, Tiny Glade, Processing, WaveFunctionCollapse, MarkovJunior, open-game-engine, DGtal, hg_sdf, Pixar's OpenUSD, Pixar's OpenSubdiv, three-gpu-pathtracer, TiltBrush, nannou, thi-ng/umbrella, toxiclibsjs, vertexshadeart, openrndr, vizhub, utymap, NVIDIA Omniverse, voxel-builder, differentiable-graphics, g9, Apparatus, sketch-n-sketch, observablehq, printeff(...), badspreadsheet, uwdata/mosaic, natto.dev, Bunkatopics, HoTT Game,
• Fantasy-Map-Generator, veloren,
• AtomicData.dev, Ink & Switch, tikzit
• Blender tools (Geometry Nodes?. etc..), gephi,
• Builder.io, pflow.dev,

Some interesting/pending questions regarding this project:

• [ ] What are mistakes in trying to spin up new projects/languages?

• [ ] What can be (partially) compiled to what using what? (Natively supported vs finding (accidental) symmetries to allow for compilation)

  • [ ] Apply this question again by loosely changing constraints?

• [ ] Compiled grammar vs analysis of runtimes?

• [ ] Just exclude the ones without open licenses. ; or if the project is big enough might as well contact all of them to lift the licenses

  Some other ways of possibly extending this list (non-completed tangents):

• [ ] Is there someone who has compiled something like this yet?

• [ ] Quick/automatic GitHub/.../Gitlab search.

• • [ ] https://proofassistants.stackexchange.com/
• • [ ] https://github.com/terkelg/awesome-creative-coding?tab=readme-ov-file
  • [ ] Through GitHub (& search elsewhere) topics: interaction-design, procedural-generation, probabilistic-programming, awesome, cellular-automata, computational-design, awesome-applied-category-theory, visualization, graph-rewriting, differentiable-rendering, gamedev, interaction-design,
  • [ ] https://github.com/Liyubov?tab=repositories
  • [ ] https://zenodo.org/communities/owseu/records?q=&l=list&p=1&s=10&sort=newest
  • [ ] "Creative coding?" - mostly some art stuff, though probably has some practical applications hidding somewhere too
  • [ ] Lot of interesting things here: https://github.com/thi-ng/umbrella?tab=readme-ov-file
  • [ ] https://iquilezles.org/articles/
  • [ ]
• • [ ] https://www.cs.ru.nl/~freek/100/
  • [ ] https://www.tptp.org/CASC/ - https://www.tptp.org/CASC/ - https://www.tptp.org/cgi-bin/SystemOnTPTP
  • [ ] https://proofwiki.org/wiki/Main_Page
  • [ ] https://proofassistants.stackexchange.com/
  • [ ] https://personal.cis.strath.ac.uk/robert.atkey/cs208/prover.html
  • [ ] https://europroofnet.github.io/tools/
  • [ ] https://wtgowers.github.io/human-style-atp/
  • [ ] https://coq-tactician.github.io/
  • [ ] https://github.com/jaalonso/Lecturas_GLC
  • [ ] https://en.wikipedia.org/wiki/Satisfiability_modulo_theories
  • [ ] https://github.com/berenoguz/Math
  • [ ] https://github.com/alexkrauss/isabelle-zf-experiments
  • [ ] https://books.google.nl/books?hl=en&lr=lang_en&id=vznnEAAAQBAJ&oi=fnd&pg=PP6&ots=JAO2M-hF-_&sig=mbPYLt3UOr6fCMEKheQQ3-sVeao&redir_esc=y#v=onepage&q&f=false
  • [ ] http://satcompetition.org/
• • [ ] https://jesper.sikanda.be/links.html
    • [ ] & similar lists of people online (i.e. followers of followers)
    • [ ] https://github.com/sw1sh
  • [ ] https://mundyreimer.github.io/blog/thermodynamics-agency-livingsystems
  • [ ] [[Jasmin Christian Blanchette]]
  • [ ] [[Simon Cruanes]]
  • [ ] Biology/Chemistry/... other fields
  • [ ] Computational Metaphysics
    • [ ] https://mally.stanford.edu/cm/
    • [ ] https://page.mi.fu-berlin.de/cbenzmueller/compmeta/htdocs/
• • [[Mealy machines]]
  • Bi-directional programming languages (Monoidal cafe?). Same with the [[Category Theory]] para lenses etc.. just the ray selection (arbitrarily branching)?

• Hardware/firmware/embedded systems etc... (TODO Actually expand this list...)

  • HSA, HIP, CUDA, firmware, .....
  • [ ] https://github.com/GPUOpen-Tools,
  • [ ] https://lists.freedesktop.org/archives/amd-gfx/2017-February/005122.html
  • [ ] https://martty.github.io/
  • [ ] https://themaister.net/blog/
  • [ ] AMD: https://gitlab.freedesktop.org/tomstdenis/umr
• • [ ] https://github.com/martinescardo/TypeTopology
  • [ ] https://scholar.archive.org/
  • [ ] https://www.semanticscholar.org/paper/TOWARDS-HIGHER-DIMENSIONAL-REWRITING-THEORY-Mimram/a88710b141afeb7bcee157e56beff635dcfb4350
  • [ ] https://github.com/cda-tum
  • [ ] https://github.com/totogo/awesome-knowledge-graph
  • [ ] Emulators, ... devkits etc..
    • [ ] https://www.synopsys.com/verification/emulation/zebu-ep1.html
  • [ ] rocm (amd)
  • [ ] https://en.wikipedia.org/wiki/STMicroelectronics
  • [ ] Tenstorrent
  • [ ] VHDL (VHSIC Hardware Description Language)
  • Compiler toolchains etc..
    • XLA
  • [ ] https://github.com/gnif/LookingGlass (... others, throughput channels ..)

• GKEYLL, simulation, emulation, render/physics/.../game engines etc..

• Some more at [[Project - (Hypergraphic) Version Control System through Rays (2024)]]

• https://www.mathstat.dal.ca/~selinger/quipper/

• All the [[PENDING (2027?+) ; Hardware, Physics]] things... String theories, ..., constructor theory etc...

  • Expand for any field

---

Some more relevant historical stuff:

• Characteristica_universalis, Lingua_generalis, Philosophical_language, Proofs_from_THE_BOOK, The_Glass_Bead_Game, Universal_language, Langlands program, Mathesis universalis

• [Phenomenology](https://en.wikipedia.org/wiki/Phenomenology_(philosophy) apparently also interested in these things

---

Some old notes for possible ways to expand the list:

Indexing existing archives/knowledge bases for preservation and possible future analysis...

• Github
• gitlab
• https://www.ietf.org/,
• Google Scholar...
• https://numenta.com/neuroscience-research/research-publications/papers/
• https://www.pnas.org/
• https://figshare.com/ (; datasets; found after toroidal topology paper)
• Kaggle.com
• arXiv dataset (https://info.arxiv.org/help/bulk_data/index.html)
• https://www.sciencedirect.com/
• other journals...
• https://iopscience.iop.org/
• https://dl.acm.org/
• https://en.wikipedia.org/wiki/MathSciNet
• https://github.com/keras-team/keras (François Chollet)
• https://github.com/CarperAI/OpenELM
• https://huggingface.co/
• https://research.tudelft.nl/en/publications/ ( other uniss.)
• (collects models & datasets;) https://github.com/intel/dffml
• Theorems/mathematics/proofs/grammers...
• https://theoretics.episciences.org/
• https://eprint.iacr.org/ Some tooling?/datasets
• https://en.wikipedia.org/wiki/Wikipedia:Database_download#Where_do_I_get_it?
• https://resources.wolframcloud.com/
• https://www.wolframphysics.org/archives/index/
• https://openlibrary.org/
• https://archiveprogram.github.com/
• https://archive.org/
• Crawling [[IPFS]]: https://github.com/adlrocha/go-libp2p-crawler
• digital library: [[JSTOR]]
• https://github.com/hartator/wayback-machine-downloader
• https://mathshistory.st-andrews.ac.uk/
• https://www.connectedpapers.com/
• https://universaldependencies.org/

---

Proof Assistant exploration, [[Proof_assistant.pdf]], [[Formal_verification.pdf]], [[Computer-assisted_proof.pdf]], [[Automated_reasoning.pdf]], [[QED_manifesto.pdf]], [[Proof_compression.pdf]] ,[[Automated_theorem_proving.pdf]], [[Compiler-compiler.pdf]],[[History_of_compiler_construction.pdf]], [[Compiler.pdf]], [[Decompiler.pdf]], [[Corrado Böhm]]

[FadiShawki]

This is probably a very relevant thing: Where invariance in this case is something like a branching ray as a cursor along a ray indicating an invariance: i.e. copies over every entry.

"Also, interesting to note might be that Von Neumann and Birkhoff attempted to ground quantum mechanics using order theory (their attempt was not very successful at that)." Me: "I think my intuition is trying to say something like. I want it ordered to talk about it usefully. But high-arity cases are probably more in line with ignoring/invariances of that order." Feb 22.

[FadiShawki]

Rays are probably a Characteristica_universalis

Some more:

[Erlang](https://en.wikipedia.org/wiki/Erlang_(programming_language), metalang99, SL, Abstract object theory (AOT), Causal graph, chemlambda, Representation theory, Lattice theory, Metamathematics, archon Ro, aUI

Some more relevant historical stuff:

Characteristica_universalis, Lingua_generalis, Philosophical_language, Proofs_from_THE_BOOK, The_Glass_Bead_Game, Universal_language, Langlands program, Mathesis universalis

[Phenomenology](https://en.wikipedia.org/wiki/Phenomenology_(philosophy) apparently also interested in these things

Some more ways to extend the list (non-completed tangents):

• [ ] https://jesper.sikanda.be/links.html
  • [ ] & similar lists of people online (i.e. followers of followers)
  • [ ] https://github.com/sw1sh
• [ ] https://mundyreimer.github.io/blog/thermodynamics-agency-livingsystems
• [ ] [[Jasmin Christian Blanchette]]
• [ ] [[Simon Cruanes]]
• [ ] Biology/Chemistry/... other fields
• [ ] Computational Metaphysics
  • [ ] https://mally.stanford.edu/cm/
  • [ ] https://page.mi.fu-berlin.de/cbenzmueller/compmeta/htdocs/

This entire thing should be compiled into a writing/study of existing stuff

• [ ] Compile into a writing

[FadiShawki]

Some old notes for possible ways to expand the list:

Indexing existing archives/knowledge bases for preservation and possible future analysis...

• Github
• gitlab
• https://www.ietf.org/,
• Google Scholar...
• https://numenta.com/neuroscience-research/research-publications/papers/
• https://www.pnas.org/
• https://figshare.com/ (; datasets; found after toroidal topology paper)
• Kaggle.com
• arXiv dataset (https://info.arxiv.org/help/bulk_data/index.html)
• https://www.sciencedirect.com/
• other journals...
• https://iopscience.iop.org/
• https://dl.acm.org/
• https://en.wikipedia.org/wiki/MathSciNet
• https://github.com/keras-team/keras (François Chollet)
• https://github.com/CarperAI/OpenELM
• https://huggingface.co/
• https://research.tudelft.nl/en/publications/ ( other uniss.)
• (collects models & datasets;) https://github.com/intel/dffml
• Theorems/mathematics/proofs/grammers...
• https://theoretics.episciences.org/
• https://eprint.iacr.org/ Some tooling?/datasets
• https://en.wikipedia.org/wiki/Wikipedia:Database_download#Where_do_I_get_it?
• https://resources.wolframcloud.com/
• https://www.wolframphysics.org/archives/index/
• https://openlibrary.org/
• https://archiveprogram.github.com/
• https://archive.org/
• Crawling [[IPFS]]: https://github.com/adlrocha/go-libp2p-crawler
• digital library: [[JSTOR]]
• https://github.com/hartator/wayback-machine-downloader
• https://mathshistory.st-andrews.ac.uk/
• https://www.connectedpapers.com/

[FadiShawki]

https://github.com/orbitmines/archive/tree/main/projects/existing-abstract-models/list

[FadiShawki]

Some Interface design / ... / visualization / game / generation projects

• Unit, Tiny Glade, Processing, WaveFunctionCollapse, MarkovJunior, open-game-engine, DGtal, hg_sdf, Pixar's OpenUSD, Pixar's OpenSubdiv, three-gpu-pathtracer, TiltBrush, nannou, thi-ng/umbrella, toxiclibsjs, vertexshadeart, openrndr, vizhub, utymap, NVIDIA Omniverse, voxel-builder, differentiable-graphics, g9, Apparatus, sketch-n-sketch, observablehq, printeff(...), badspreadsheet, uwdata/mosaic, natto.dev, Bunkatopics,
• Fantasy-Map-Generator, veloren,

Possible extensions:

• [ ] https://github.com/terkelg/awesome-creative-coding?tab=readme-ov-file

• [ ] Through GitHub (& search elsewhere) topics: interaction-design, procedural-generation, probabilistic-programming, awesome, cellular-automata, computational-design, awesome-applied-category-theory, visualization, graph-rewriting, differentiable-rendering, gamedev, interaction-design,

• [ ] https://github.com/Liyubov?tab=repositories

• [ ] https://zenodo.org/communities/owseu/records?q=&l=list&p=1&s=10&sort=newest

• [ ] "Creative coding?" - mostly some art stuff, though probably has some practical applications hidding somewhere too

• [ ] Lot of interesting things here: https://github.com/thi-ng/umbrella?tab=readme-ov-file

• [ ] https://iquilezles.org/articles/

• [ ] https://en.wikipedia.org/wiki/Probabilistic_programming

  • [ ] Analytica, bayesloop, Bean Machine, CuPPL, Venture, Probabilistic-C, Anglican, IBAL, BayesDB, PRISM, Infer.NET, dimple, chimple, BLOG, diff-SAT, PSQL, BUGS, FACTORIE, PMTK, Alchemy, Dyna, Figaro, Church, ProbLog, ProBT, Stan, Hakaru, BAli-Phy, ProbCog, Gamble, PWhile, Tuffy, PyMC, Rainier, greta, pomegranate, Lea, WebPPL, Let's Chance, Picture, Turing.jl, Low-level First-order PPL, Troll, Edward, TensorFlow Probability, Edward2, Pyro, NumPyro, Saul, RankPL, Birch, PSI, Blang, MultiVerse

• [ ]

• Spectral graph theory, Python: wolfram_model, SetReplace, hypercore-decomposition, higher-order-motifs, XGI, hypergraphx, Probabilistic programming, BoomFilters, MJr, Agents.jl, particle-life, Lenia, The-Powder-Toy, Procedural generation,

[FadiShawki]

• liquidsoap, The Munich Quantum Toolkit (MQT),

Interface..

• Blender tools (Geometry Nodes?. etc..), gephi,

more expansions...

• [ ] https://github.com/martinescardo/TypeTopology
• [ ] https://scholar.archive.org/
• [ ] https://www.semanticscholar.org/paper/TOWARDS-HIGHER-DIMENSIONAL-REWRITING-THEORY-Mimram/a88710b141afeb7bcee157e56beff635dcfb4350
• [ ] https://github.com/cda-tum
• [ ] https://github.com/totogo/awesome-knowledge-graph

[FadiShawki]

I'll organize this properly later

Interface... AtomicData.dev, Ink & Switch, tikzit

.... Solid,

Chemistry: Assembly Theory

More expansions

• [ ] https://www.cl.cam.ac.uk/~jdy22/projects/frex/

---

• [ ] Whole project makes it necessary to get the practical low-level systems in this too.

  • [ ] Lookup existing projects in that space, decompilers, interfaces for binary analysis etc..

• HoTT Game,

[FadiShawki]

• [[Mealy machines]]
• Bi-directional programming languages (Monoidal cafe?). Same with the [[Category Theory]] para lenses etc.. just the ray selection (arbitrarily branching)?

Hardware/firmware/embedded systems etc... TODO Actually expand this list... HSA, HIP, CUDA, firmware, .....

• [ ] https://github.com/GPUOpen-Tools,
• [ ] https://lists.freedesktop.org/archives/amd-gfx/2017-February/005122.html
• [ ] https://martty.github.io/
• [ ] https://themaister.net/blog/
• [ ] AMD: https://gitlab.freedesktop.org/tomstdenis/umr
• [ ]

expand...

• [ ] https://proofassistants.stackexchange.com/

[FadiShawki]

Moved the project from my archive to a separate repository. Minimal language implementations will still be in the universal language repo, but anything else about this project I'll throw in here: https://github.com/orbitmines/library