4 releases
0.2.2 | Mar 23, 2022 |
---|---|
0.2.1 | Mar 23, 2022 |
0.2.0 | Mar 23, 2022 |
0.1.0 | Mar 23, 2022 |
#1339 in Math
23 downloads per month
41KB
832 lines
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:
- Parse expression
- Construct commutative square
- Expand knowledge about morphisms using rules for Category Theory
- Analyze new knowledge and reintegrate it into the commutative square
- Synthesize expression.
Dependencies
~330KB