### 4 releases

0.2.2 | Jul 30, 2019 |
---|---|

0.2.1 | May 15, 2019 |

0.2.0 | Nov 19, 2018 |

0.1.0 | Nov 15, 2018 |

#**827** in Algorithms

**26** downloads per month

Used in reachability_solver

**MIT**license

25KB

163 lines

# linear_solver

A linear solver designed to be easy to use with Rust enums.

This is a library for automated theorem proving.

Linear solving means that some facts can be replaced with others. This technique can also be used to make theorem proving more efficient.

If you are looking for a solver that does not remove facts,

see monotonic_solver

*Notice! This solver does not support multiple histories.
It assumes that when facts are simplified,
they prove the same set of facts without the simplifaction.*

A linear solver can be used to:

- Prove some things in linear logic
- Prove some things in classical logic more efficiently
- Prove some things about where resources are "consumed"
- Constraint solving
- Implement some constraint solving programming language

This project was heavily inspired by CHR (Constraint Handling Rules)

### Example: Walk

`/*`
In this example, we reduce a walk (left, right, up, down):
l, l, u, l, r, d, d, r
----------------------
l, u
`*/`
`extern` `crate` linear_solver`;`
`use` `linear_solver``::``{`solve_minimum`,` Inference`}``;`
`use` `linear_solver``::``Inference``::``*``;`
`use` `std``::``collections``::`HashSet`;`
`use` `self``::``Expr``::``*``;`
`#``[``derive``(``Clone``,` PartialEq`,` Eq`,` Debug`,` Hash`)``]`
`pub` `enum` `Expr` `{`
Left`,`
Right`,`
Up`,`
Down`,`
`}`
`pub` `fn` `infer``(``cache``:` `&``HashSet``<`Expr`>`, `_facts``:` `&`[Expr]`)`` ``->` `Option``<`Inference`<`Expr`>``>` `{`
`//` Put simplification rules first to find simplest set of facts.
`if` cache`.``contains``(``&`Left`)` `&&` cache`.``contains``(``&`Right`)` `{`
`return` `Some``(`ManyTrue `{`from`:` `vec!``[`Left`,` Right`]``}``)``;`
`}`
`if` cache`.``contains``(``&`Up`)` `&&` cache`.``contains``(``&`Down`)` `{`
`return` `Some``(`ManyTrue `{`from`:` `vec!``[`Up`,` Down`]``}``)``;`
`}`
`None`
`}`
`fn` `main``(``)`` ``{`
`let` start `=` `vec!``[`
Left`,`
Left`,`
Up`,`
Left`,`
Right`,`
Down`,`
Down`,`
Right`,`
`]``;`
`let` res `=` `solve_minimum``(`start`,` infer`)``;`
`for` i `in` `0``..`res`.``len``(``)` `{`
`println!``(``"``{:?}``"``,` res`[`i`]``)``;`
`}`
`}`

### Example: Less or Equal

`/*`
In this example, we prove the following:
X <= Y
Y <= Z
Z <= X
------
Y = Z
Y = X
`*/`
`extern` `crate` linear_solver`;`
`use` `linear_solver``::``{`solve_minimum`,` Inference`}``;`
`use` `linear_solver``::``Inference``::``*``;`
`use` `std``::``collections``::`HashSet`;`
`use` `self``::``Expr``::``*``;`
`#``[``derive``(``Clone``,` PartialEq`,` Eq`,` Debug`,` Hash`)``]`
`pub` `enum` `Expr` `{`
Var`(``&``'static` `str``)``,`
Le`(``Box``<`Expr`>``,` `Box``<`Expr`>``)``,`
`Eq``(``Box``<`Expr`>``,` `Box``<`Expr`>``)``,`
`}`
`pub` `fn` `infer``(``cache``:` `&``HashSet``<`Expr`>`, `facts``:` `&`[Expr]`)`` ``->` `Option``<`Inference`<`Expr`>``>` `{`
`//` Put simplification rules first to find simplest set of facts.
`for` ea `in` facts `{`
`if` `let` Le`(``ref` a`,` `ref` b`)` `=` `*`ea `{`
`if` a `==` b `{`
`//` (X <= X) <=> true
`return` `Some``(`OneTrue `{`from`:` ea`.``clone``(``)``}``)``;`
`}`
`for` eb `in` facts `{`
`if` `let` Le`(``ref` c`,` `ref` d`)` `=` `*`eb `{`
`if` a `==` d `&&` b `==` c `{`
`//` (X <= Y) ∧ (Y <= X) <=> (X = Y)
`return` `Some``(``Inference``::`replace`(`
`vec!``[`ea`.``clone``(``)``,` eb`.``clone``(``)``]``,`
`Eq``(`a`.``clone``(``)``,` b`.``clone``(``)``)``,`
cache
`)``)`
`}`
`}`
`}`
`}`
`if` `let` `Eq``(``ref` a`,` `ref` b`)` `=` `*`ea `{`
`for` eb `in` facts `{`
`if` `let` Le`(``ref` c`,` `ref` d`)` `=` `*`eb `{`
`if` c `==` b `{`
`//` (X = Y) ∧ (Y <= Z) <=> (X = Y) ∧ (X <= Z)
`return` `Some``(``Inference``::`replace_one`(`
eb`.``clone``(``)``,`
Le`(`a`.``clone``(``)``,` d`.``clone``(``)``)``,`
cache
`)``)``;`
`}` `else` `if` d `==` b `{`
`//` (X = Y) ∧ (Z <= Y) <=> (X = Y) ∧ (Z <= X)
`return` `Some``(``Inference``::`replace_one`(`
eb`.``clone``(``)``,`
Le`(`c`.``clone``(``)``,` a`.``clone``(``)``)``,`
cache
`)``)``;`
`}`
`}`
`if` `let` `Eq``(``ref` c`,` `ref` d`)` `=` `*`eb `{`
`if` b `==` c `{`
`//` (X = Y) ∧ (Y = Z) <=> (X = Y) ∧ (X = Z)
`return` `Some``(``Inference``::`replace_one`(`
eb`.``clone``(``)``,`
`Eq``(`a`.``clone``(``)``,` d`.``clone``(``)``)``,`
cache
`)``)``;`
`}`
`}`
`}`
`}`
`}`
`//` Put propagation rules last to find simplest set of facts.
`for` ea `in` facts `{`
`if` `let` Le`(``ref` a`,` `ref` b`)` `=` `*`ea `{`
`for` eb `in` facts `{`
`if` `let` Le`(``ref` c`,` `ref` d`)` `=` `*`eb `{`
`if` b `==` c `{`
`//` (X <= Y) ∧ (Y <= Z) => (X <= Z)
`let` new_expr `=` Le`(`a`.``clone``(``)``,` d`.``clone``(``)``)``;`
`if` `!`cache`.``contains``(``&`new_expr`)` `{``return` `Some``(`Propagate`(`new_expr`)``)``}``;`
`}`
`}`
`}`
`}`
`}`
`None`
`}`
`pub` `fn` `var``(``name``:` `&``'static` `str``)`` ``->` `Box``<`Expr`>` `{``Box``::`new`(`Var`(`name`)``)``}`
`fn` `main``(``)`` ``{`
`let` start `=` `vec!``[`
Le`(``var``(``"`X`"``)``,` `var``(``"`Y`"``)``)``,` `//` X <= Y
Le`(``var``(``"`Y`"``)``,` `var``(``"`Z`"``)``)``,` `//` Y <= Z
Le`(``var``(``"`Z`"``)``,` `var``(``"`X`"``)``)``,` `//` Z <= X
`]``;`
`let` res `=` `solve_minimum``(`start`,` infer`)``;`
`for` i `in` `0``..`res`.``len``(``)` `{`
`println!``(``"``{:?}``"``,` res`[`i`]``)``;`
`}`
`}`

### Linear logic

When some facts are simplified, e.g.:

`X, Y <=> Z
`

You need two new copies of

and `X`

to infer another `Y`

.
This is because the solver does not remove all copies.`Z`

When doing classical theorem proving with a linear solver,
it is common to check that every fact is unique in the input,
and that the

is checked before adding new facts.
This ensures that the solver does not add redundant facts.`cache`

However, when doing linear theorem proving,
one can generate redundant facts

for every `Z`

and `X`

.`Y`

### Meaning of goals

Since a linear solver can both introduce new facts and remove them, it means that termination in the sense of proving a goal does not make sense, since the goal can be removed later.

Instead, a goal is considered proved when it belongs to the same "cycle". This is the repeated list of sets of facts that follows from using a deterministic solver with rules that stops expanding.

The minimum set of facts in the cycle is considered the implicit goal, because all the other facts in the cycle can be inferred from this set of facts.

Notice that this a minimum set of facts in a cycle is different from a minimum set of axioms. A minimum set of axioms is a set of facts that proves a minimum set of facts with even fewer facts. With other words, the minimum set of axioms starts outside the cycle. When it moves inside the cycle, it is identical to some minimum set of facts.

Both the minimum set of facts and the minimum set of axioms can be used to identify an equivalence between two sets of facts.

### Intuition of `false`

and `true`

`false`

`true`The intuition of

can be thought of as:`false`

- Some fact which everything can be proven from
- Some fact which every contradiction can be simplified to
- A language that contains a contradiction for every truth value

The minimum set of facts in a such language,
when a cycle contains

, is `false`

.`false`

The intuition of

can be thought of as:`true`

- Some fact which every initial fact can be proven from.
- Some fact that contradicts
`false`

This means that the initial facts implies

and
since it contradicts `true`

, if there exists a contradiction
in the initial facts, then they can prove `false`

.`false`

Therefore a proof from initial facts is

if it's minimum set of facts does not equals `true`

.`false`

#### Dependencies

~555KB