Crate caso

Crate caso 

Source
Expand description

§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.

MorphismNotation
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.