ggleason

Write it in a theorem prover! No really!

It's really incredible. We decided to see if we could write a Tokio-like library in Lean and were able to do it in a week with performance similar to Node 22. There is really no reason not to use a theorem prover now instead of a functional programming language, and soon it will be better than most languages. All that will remain that it can't do are the jobs of low level languages like C++ [for now].

If you write it in a theorem prover you can have the LLM write proofs about the code quite easily. Lean is easily good enough to compete with javascript, so now I think it makes sense to switch to Lean.

How to use supervised learned classifiers without a training set by using LLMs.

It would be extremely handy to have a document store / graph database which had row polymorphism. I started writing a prototype, but unfortunately never got there. I wonder if any such things already exist?

Those are all interesting ideas.

For the index structure itself you can use succinct dynamic data structures to reduce the size. The bulk loading approach is particularly amenable to use of succinct data structures as the node-vectors in a HNSW are montonic they can use an Elias-Fano encoding. The neighborhoods can use log-arrays.

Creating a multi-index also seems possible, where you use the triangle-inequality to prune the candidate vectors. This will probably require storing the distances for neighbor distances in the bottom layer, in order to be time-efficient for query and would thereby be slightly bigger. I haven't tried it yet but I intend to.

There is also the possibility of using random projection for dimensionality reduction. I also haven't tried this yet either but will give it a go soon. We haven't folded the parallel hnsw into our open source VectorLink yet, but we'll be doing it in the near future - we wanted a little bit of stability of approach first.

TerminusDB founder here. TerminusDB is now at the absolute outer edge of compact data representation. Neo4j is literally 10 times more space for the same data meaning that you'll need 10 times as much memory for a big graph. Succinct datatypes will have their day yet.

Oh, I should probably mention a blog I wrote describing how it works: https://github.com/terminusdb/technical-blogs/blob/main/blog...

I was looking at various forms of indexing solutions to solve search and clustering problems with TerminusDB for clients. When I compared solutions against embeddings from LLMs, they LLMs were just far easier to work with and got much better results. I believe traditional text indexing will die quickly, as will a lot of the Entity Resolution and traditional clustering methods to be replaced completely by LLM's. We found them so compelling we wrote our own open source vector database sidecar: https://github.com/terminusdb-labs/terminusdb-semantic-index...

TerminusDB represents the data using succinct data structures which reduces the required memory substantially over many other representations. Each branch needs to be capable of being loaded into memory completely - but individual revisions are loaded separately.

Diffs can be constructed between two objects, or you can get sets of diffs of objects between commits automatically. You can manually construct diffs and use them to patch branches.

We don't have a conversion tool from SQL database tables, but it's something on my list.

Yeah, it's really unfortunate that these amazing advances in datalog don't make it into general purpose languages.

> Datomic Cloud is slow, expensive, resource intensive, designed in the baroque style of massively over-complicated CloudFormation astronautics. Hard to diagnose performance issues. Impossible to backup.

You should give TerminusDB a go (https://terminusdb.com/), it's really OSS, the cloud version is cheap, fast, there are not tons of baroque settings, and it's easy to backup using clone.

TermiusDB is a graph database with a git-like model with push/pull/clone semantics as well as a datalog.

Hi this is Gavin and I founded TerminusCMS (terminusdb.com).

CMS stands for "content management system" and headless means API-based, with no restrictions over where you use the content. Devs are you folks.

Existing headless CMS tools sometimes make it up as they go along - starting with the idea of ‘I want to build a company that delivers a headless CMS’ and then quickly slapping a bunch of technologies together and ending up with a pile of JSONs floating around a MongoDB or another similar frankenstein. As we’d already built the document graph data layer from the ground up, we could properly integrate the CMS features to give a seamless developer experience. We are never going to send you to a screen that says, ‘TerminusCRM requires NodeJS version 10+ and a Mongo database’. It is all contained in one in-memory, highly compressed data management system that we designed and built for this specific purpose.

A few of the other offerings are just headless markdown backed by git - which is actually a good idea, but comes with the capacity and performance limitations that git implies.

Why not have a highly performant document graph content management system that incorporates the most important concepts from git in the data layer? All the version control features that content needs (clone, push, pull, branch, revert, merge) and are highly awkward in other systems.

We also thought that GraphQL was the obvious data manipulation choice for content, but found weak implementations wherever we looked. For TerminusCMS, we’ve implemented a suite of features which allows you to query a TerminusCMS project using GraphQL in such a way that deep linking can be discovered. We can use path queries with GraphQL.

To summarize our market thoughts - it seems that devs want: * Deploy anywhere open-source * Dev-first in memory, highly compressed, scalable and fast content management so you can build complex and fully featured web apps of every shape and size * Git-like features to help with permissions and version control (and - crucially - merge) * Best-in-class GraphQL implementation

And there was nothing offering that mix until we released TerminusCMS.

TerminusCMS is a content platform that sits at the convergence of content and knowledge. It is a model-driven, API-first approach to content management. With TerminusCMS you can use your data as content. The data employed in content has meanings associated with it, and because that content is well structured, the content can also be used as if it were data — in fact, that content is data. TerminusCMS is structured like Git, so you get all the git-like features for your content engine. History, change management, branching, non-linear development, easy backups, distributed development, and more. You can enrich your content with semantics which can give you the ability to personalize content and build superior recommender and AI/ML systems.

Content curation needs change requests: you need to be able to add a new translation, or new content in a branch, which is viewable as an entire site, but which only goes into production when you "merge to main". TerminusCMS gives devs a powerful way to define schema, query, deliver content and assets to front end. It has schema-as-code; is standards-based for interoperability; has an extremely fast publishing API; and provides workflows made by way of content and network model, not wired into product itself. It give editors a way to manage content automatically so that devs don't need to do much to support them. You can use TerminusCMS to build your complex app, or to manage your organization knowledge.

TerminusCMS is open-source all the way down, so if we vanish or piss you off, you can recover and continue.

The business is cloud hosting and enterprise delivery, which we hope can keep the wolf from the door. It is freemium with a generous free tier and easily cloned examples, so take a look.

This blog gives some details of how to order a wide variety of different data types using lexical embeddings. This is very useful for TerminusDB as we use dictionary structures to represent ids, but it would also be relevant in radix trees or other database structures that rely on sharing of prefixes.

Yes, but the low level memory layout and search iterators are written in rust.

Quite speedy, especially when looking at relatively long chains in the graph.

This is my account of how we took the idea of succinct data structures, and added mutability, thereby getting something which allows for git-like functionality, but also fast query and compact memory footprint.

Well, I do know SPARQL :D

TerminusDB uses a datalog under the hood, but GraphQL can expose a lot of datalog like power with the right interface. Ultimately we want to have named parameteric queries in datalog exposing "pseudo-edges" in GraphQL which can be treated just like a normal field but are actually calculated.

Juniper helped us implement a GraphQL / RDF bridge in about two weeks.

I am of the same opinion. TerminusDB uses a data log for query and update. I think it will catch on.

And in the future we will even be able to add constraints - which can be a real superpower in querying graphs.

Well, in one sense the are directly interconvertable. The documents in TerminusDB are elaborated to JSON-LD internally during type-checking and inference.

However, it's not just a question of whether one can be made into another. The use of contexts is very cumbersome, since you need to specify different contexts at different properties for different types. It makes far more sense to simply have a schema and perform the elaboration from there. Plus without an infrastructure for keys, Ids become extremely cumbersome. So beyond just type decorations on the leaves, It's the difference between:

  {
    "general_variables": {
      "alternative_name": ["Sadozai Kingdom", "Last Afghan Empire" ],
      "language":"latin"
    },
    "name":"AfDurrn",
    "social_complexity_variables": {
      "hierarchical_complexity": {"admin_levels":"five"},
      "information": {"articles":"present"}
    },
    "warfare_variables": {
      "military_technologies": {
        "atlatl":"present",
        "battle_axes":"present",
        "breastplates":"present"
      }
    }
  }

And

  {
    "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11",
    "@type":"Polity",
    "general_variables": {
      "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/general_variables/GeneralVariables/e4360ee3766c2863f06a34ffcdd9869d41b03d04c6f6af5f94b0a14a47e8e704",
      "@type":"GeneralVariables",
      "alternative_name": ["Last Afghan Empire", "Sadozai Kingdom" ],
      "language":"latin"
    },
    "name":"AfDurrn",
    "social_complexity_variables": {
      "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/social_complexity_variables/SocialComplexityVariables/191353c4b7138842ec4029dd07fbd63c9dda752f0cd72b1584f046a274cf024c",
      "@type":"SocialComplexityVariables",
      "hierarchical_complexity": {
        "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/social_complexity_variables/Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/social_complexity_variables/SocialComplexityVariables/191353c4b7138842ec4029dd07fbd63c9dda752f0cd72b1584f046a274cf024c/hierarchical_complexity/HierarchicalComplexity/d6a772c5c6919cc511a24ab89f908032aa32b1e3e939d2e0c32044b3a5d9151d",
        "@type":"HierarchicalComplexity",
        "admin_levels":"five"
      },
      "information": {
        "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/social_complexity_variables/Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/social_complexity_variables/SocialComplexityVariables/191353c4b7138842ec4029dd07fbd63c9dda752f0cd72b1584f046a274cf024c/information/Information/2f557c1016552f30b8d8bb1bdd9a8584791dd06d32f25bded86a7eb59788ea7f",
        "@type":"Information",
        "articles":"present"
      }
    },
    "warfare_variables": {
      "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/warfare_variables/WarfareVariables/704a2c1854a2fe80616fbea0ef0dcd6ce47f5174529ca191617e42397108c437",
      "@type":"WarfareVariables",
      "military_technologies": {
        "@id":"Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/warfare_variables/Polity/7286b191f5f62a05290b8961fd8836a26ddc8399611b216fae4aaacc58ba6c11/warfare_variables/WarfareVariables/704a2c1854a2fe80616fbea0ef0dcd6ce47f5174529ca191617e42397108c437/military_technologies/MilitaryTechnologies/80a91b3e5381154387bde4afc66fdd38834de16c671c49c769f5244475cbbb1b",
        "@type":"MilitaryTechnologies",
        "atlatl":"present",
        "battle_axes":"present",
        "breastplates":"present"
      }
    }
  }

I wrote it from scratch 2 days ago.

That's discussed in the article though. The open world assumption is untenable. Having shareable interoperable schemata that can refer to each-other safely would be a god send however. And that's what is currently very hard but needn't be.

That's a very good point re SAT/SMT. F* (https://www.fstar-lang.org/) has done truly amazing things by making use of them, and it's great to be able to get sophisticated correctness checks while doing basically non of the work.

I'm going to have to go away and think about how one could effectively leverage this in a data setting, but I'd love to hear ideas.

Prolog is still the best query language out there. If it had as much attention as other languages like python or javascript, we'd have some real space-age programming systems.

TerminusDB CTO here.

Echoing what triska said, CLP(ℤ) and friends are some of the most under-appreciated aspects of prolog implementations.

I'm amazed that programmers still don't have access to CLP when trying to do scheduling and planning solutions.

As an example in practice, what if you want to know about a transaction in which a number of entities transitively had holdings in one of the beneficiaries of the transaction at that particular time. The date window is not known, and the date windows are important in the ownership chain as well as the transactions that are being undertaken.

With CLP(FD) you can ask for a window of time, and the solution will zoom in on an appropriate time window which exists for the entire chain and match the time of the transaction.

Now try to do this query in SQL. It's almost impossibly hard.

I can't wait until I have the time to implement constraint variables for TerminusDB, but at the minute we are still working on more prosaic features.

Aside from that there are very interesting program correctness and optimisation systems which are based on prolog (usually a datalog). For instance Soufflé: https://souffle-lang.github.io