CT for all : we can make a Universal Knowledge Interface

General
1

Category theory holds great potential,
but today the language is only shared by a very small part of humanity.
How can we open this way of thinking to everyone?

There is a possibility beyond gradual education:
we can make a universal knowledge interface
— in the embodied form of CT as visual logic —
that enables people to think holistically, openly, creatively
simply by interactively exploring, building, and sharing knowledge.

Many in ACT know string diagrams are intuitive and powerful, but so far we’ve only really developed those for various kinds of categories.
Logic is modelled by a fibered category,
because a category of predicates and entailments
depends on a category of types and processes.
My thesis defined the string diagrams of fibered categories, “visual logic”;
and by creating its interface, I think we can make a canvas for the mind.

Here’s where the rubber meets the road:
the whole world now runs on knowledge, just with bad UI.
A database is a logic:
a table is a predicate over some column types, and
an update rule is an entailment over some program.

A predicate of some types is a node that connects wires,
embodying the idea that knowledge is connection,
and all logical constructions are expressed by simple visual operations.

node-table
node-table3238×1014 104 KB

All basic data events fit into this framework:

  • create : update 1 → T
  • modify : update T → T
  • delete : update T → 0
  • transfer : update T0 → T1
  • query : construct predicates from logic operations

A transfer is an update between databases: a fibered profunctor.
All data processing and sharing is an instance of this structure —
a system of programs between datatypes, and rules between tables.

transfer
transfer1986×1222 49 KB

I am starting a company, to make a universal data interface,
under the working name of Hold that Thought.
The data tool market size is many billions of dollars,
and yet these tools still require complicated syntax like SQL.
Most people would much rather connect two wires
than type "SELECT c FROM t JOIN … "

I’m writing an SBIR grant to the NSF.
I’m confident in the idea, but alone it is too big to properly begin.
The first needs are funding, and someone experienced in UI+DB;
but this is just my current plan so far, still very new
— I look forward to next week’s conference.
With the right connections, it could grow fast and bring big $$$ to ACT.

At this point, I think the hour is very late…
for all our big dreams, I think it’s now or never.
More than convincing anyone,
I just want to meet with those who might see what I see.
Let me know! Thanks for reading.

2 Likes
2

It seems like a nitpicky detail, but I think that the entire “logic and databases are the same thing” premise needs to have a good story for handling the fact that a table in a database stores a finitely-supported relation, but in logic we usually work with relations of non-finite support, presented symbolically.

Category theory is only useful for computing in as much as it organizes real algorithms. Where are the algorithms for the logical operations that are agnostic to symbolically presented/finitely presented propositions?

I have every confidence that such algorithms could be found. But I would say that this vision looks a lot more real once they are pinned down and demoed.

2 Likes
3

Say we have a table of numbers called One, with a single row “1”, and we form not(One). That’s fine; it still works as a predicate to evaluate on numbers. But if we try to display this table, or apply some program, then a bubble can pop up and says “hey, this is infinite! how do you want to handle it?” and then gives the parameters to configure. The “virtual” database is a genuine logic; and it’s just the physical part that’s finite, yet changing to faithfully simulate the whole.

Does that make sense? What problems do you have in mind?

We talked about this on a video call, and I said the same thing. You haven’t yet described a specific problem, just raised general concern about finitude. Sure, it generally makes sense that there’s probably a good amount to do there. The whole thing is a huge undertaking, with tons of challenges; so the more input the better.

[Probably the biggest research question I know so far: cartesian bifibered profunctors are straightforward to define, but the incorporation of closed structure is less obvious. That’s the difference between having a multiverse of FOLs vs one of HOLs. Besides the basics in my thesis, the whole theory of fibered profunctors is unexplored, and these are meant to form the basis for sharing between databases.]