Crate caso

Caso

Category Theory Solver for Commutative Diagrams.

=== Caso 0.2 ===
Type `help` for more information.
> (A <-> B)[(A <-> C) -> (B <-> D)] <=> (C -> D)
(A <-> B)[(A <-> C) -> (B <-> D)] <=> (C <-> D)

To run Case from your Terminal, type:

cargo install --example caso caso

Then, to run:

caso

Syntax

A commuative diagram in Caso is written in the following grammar:

<left>[<top> -> <bottom>] <=> <right>

This syntax is based on the notation for Path Semantics.

Caso automatically corrects directional errors, e.g. when you type (a -> b)[(c -> a) -> ...] <=> .... the c is wrong relative to a, so, Caso corrects this to (a -> b)[(a <- c) -> ...] <=> ....

Higher morpisms are supported by counting - (1) and = (2) in the arrow. For example, <-> is a 1-isomorphism and <=> is a 2-isomorphism.

Morphism	Notation
Directional	->
Reverse Directional	<-
Epi	->>
Reverse Epi	<<-
Mono	!->
Reverse Mono	<-!
Right Inverse	<->>
Left Inverse	<<->
Epi-Mono	!->>
Reverse Epi-Mono	<<-!
Iso	<->
Zero	<>

How to solve triangles

Triangles can be expanded into commutative square using identity morphisms.

For example:

> (A <-> B)[(A -> C) -> (B -> C)] <=> (C -> C)
(A <-> B)[(A -> C) -> (B -> C)] <=> (C <-> C)

Here, C -> C is an identity morphism from C to itself.

Design

Caso uses Avalog as monotonic solver.

The Avalog rules are located in “assets/cat.txt”.

The automated theorem prover uses the following steps:

1. Parse expression
2. Construct commutative square
3. Expand knowledge about morphisms using rules for Category Theory
4. Analyze new knowledge and reintegrate it into the commutative square
5. Synthesize expression.

Modules

code

Commutative diagram solver.

parsing

Parse syntax.

sym

Data structure for symbols in Avalog solver.

Enums

Expr

Stores Caso expression.

Morphism

Represents a morphism.

Functions

conv

Converts string into expression (panics when format is invalid).

dir

Directional e.g. A -> B.

dir_n

Higher directional e.g. A => B.

epi

Epi e.g. A ->> B.

epi_mono

Epi-mono e.g. A !->> B.

epi_mono_n

Higher epi-mono e.g. A !=>> B.

epi_n

Higher epi e.g. A =>> B.

iso

Iso e.g. A <-> B.

iso_n

Higher iso e.g. A <=> B.

mono

Mono e.g. A !-> B.

mono_n

Higher mono e.g. A !=> B.

path

A path e.g. X[Y].

rev_epi

Reverse epi-mono e.g. A <<-! B.

rev_epi_n

Reverse epi-mono e.g. A <<=! B.

rev_mono

Reverse mono e.g. A <-! B.

rev_mono_n

Higher reverse mono e.g. A <=! B.

rev_right_inv

Reverse right inverse e.g. A <<-> B.

rev_right_inv_n

Higher reverse right inverse e.g. A <<=> B.

right_inv

Right inverse e.g. A <->> B.

right_inv_n

Higher right inverse e.g. A <=>> B.

solve_str

Solve a string.

zero

Zero e.g. A <> B.

zero_n

Higher zero.