Skip to content
The methodOpen data
Back to the collection

Knowledge Representation in Bicategories of Relations

Evan Patterson

2017 · arXiv

DatabasesMathematicsProgramming languages
Read the paper
HN score
0
Mentions
4
Readers
3
Months
4
What’s in a score?

From the abstract

We introduce the relational ontology log, or relational olog, a knowledge representation system based on the category of sets and relations. It is inspired by Spivak and Kent's olog, a recent categorical framework for knowledge representation. Relational ologs interpolate between ologs and description logic, the dominant formalism for knowledge representation today. In this paper, we investigate relational ologs both for their own sake and to gain insight into the relationship between the algebraic and logical approaches to knowledge representation. On a practical level, we show by example that relational ologs have a friendly and intuitive--yet fully precise--graphical syntax, derived from the string diagrams of monoidal categories. We explain several other useful features of relational ologs not possessed by most description logics, such as a type system and a rich, flexible notion of instance data. In a more theoretical vein, we draw on categorical logic to show how relational ologs can be translated to and from logical theories in a fragment of first-order logic. Although we make extensive use of categorical language, this paper is designed to be self-contained and has considerable expository content. The only prerequisites are knowledge of first-order logic and the rudiments of category theory.

Metadata: arXiv. Abstracts retain their original authors’ rights.

In the conversation

Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels

4 selected excerpts · 4 total mentions

lidHanteyk
Neutral mention · rule
Haskell is not really category-theoretic. The category Hask doesn't quite line up with real-world Haskell. The disconnection is well-understood and well-documented [0][1]. Category theory can directly give us systems from theories. See the papers behind FQL/CQL for more details, especially [2] and [3]. [0] https://wiki.haskell.org/Hask [1] http://www.cse.chalmers.se/~nad/publications/danielsson-et-a... [2] https://arxiv.org/abs/1102.1889v2 [3] https://arxiv.org/abs/1706.00526
Original comment Software Architecture Guide
myWindoonn
Neutral mention · rule
Mathematics is metaphysics. I'd like your refutation to center on any nuance which might separate the two disciplines other than the sad fact that many philosophers don't learn much maths. Logic is metaphysics: https://philpapers.org/archive/ALVLIM-3.pdf Logic is mathematical, logic is categorical (structured in a deep way amenable to category theory), maths is categorical: http://math.ucr.edu/home/baez/rosetta.pdf https://ncatlab.org/nlab/show/internal+logic https://ncatlab.org/nlab/show/topos Ontology is categorical: https://arxiv.org/abs/1102.1889v2 https://arxiv.org/abs/1706.00526 The working programmer is an ontologist and a taxonomist, but this fact isn't well-understood.
Original comment A Formal Apology for Metaphysics [pdf]
DonbunEf7
Neutral mention · rule
You seem intelligent, so I'm going to drop you into the deep end. In category theory, a topos [0][1] (plural topoi) is a structure-place where logic can be done. Boolean logic corresponds to a particular topos. Actually, there are at least two topoi which do Boolean logic; one of them has the law of excluded middle, and another has the axiom of choice. [2] And there's an infinite other number of topoi to choose from! Topoi can be custom-made to categorical specifications. We can insist that there are three truth values, and then we can use a topos construction to determine what the resulting logical connectives look like. [3] Finally, there are logical systems which are…
Read the full comment
too weak to have topoi. These are the fragments, things like regular logic [4] or Presburger arithmetic. To address your second argument, why do we work in a world with Boolean logic? Well, classical computers are Boolean. Why? Because we invented classical computing in a time where Boolean logic was the dominant logic, and it fits together well with information and signal theory, and most importantly because we discovered a not-quite-magical method for cooking rocks in a specific way which creates a highly-compact semiconductor-powered transistor-laden computer. Computers could be non-Boolean. If you think that the brain is a creative computer, then the brain's model of computation is undeniably physical and non-classical. It's possible, just different. Oh, and even if Boolean logic is the way of the world, does that really mean that all propositions are true or false? Gödel, Turing, Quine, etc. would have a word with you! [0] https://en.wikipedia.org/wiki/Topos#Elementary_topoi_(topoi_... [1] https://ncatlab.org/nlab/show/topos [2] https://ncatlab.org/nlab/show/two-valued+logic [3] https://toposblog.org/2018/01/15/some-simple-examples/ [4] https://arxiv.org/abs/1706.00526
Original comment The Logical Disaster of Null
myWindoonn
Neutral mention · rule
Unfortunately, Kialo does not have any features for structural reasoning, where the logical connections between arguments are completely formalized and precise. It relies on a human element to check each argument. Edit: How to do this formally? Look at formal systems for hints of how to do it in the 1900s, or category theory for how to do it in the modern day. [0][1] [0] https://arxiv.org/abs/1102.1889v2 [1] https://arxiv.org/abs/1706.00526
Original comment Kialo – a platform for rational debate

Keep following the thread.

More in Databases

More from the same topics.

1994arXiv

On proof and progress in mathematics

William P. Thurston

In response to Jaffe and Quinn [math.HO/9307227], the author discusses forms of progress in mathematics that are not captured by formal proofs of theorems, especially in his own work in the theory of foliations and geometrization of 3-manifolds and dynamical systems.

Mathematics
29 mentions21 months
9HN score
2017arXiv

The Case for Learned Index Structures

Tim Kraska, Alex Beutel, Ed H. Chi +2

Indexes are models: a B-Tree-Index can be seen as a model to map a key to the position of a record within a sorted array, a Hash-Index as a model to map a key to a position of a record within an unsorted array, and a BitMap-Index as a model to indicate if a data record exists or not.

Databases
19 mentions14 months
5HN score