33 lines
1.3 KiB
Markdown
33 lines
1.3 KiB
Markdown
# Cyclic proofs and sappho
|
|
|
|
It seems that cyclic proofs and sappho would be a good fit. The decision
|
|
process of sappho's subtyping relation is based on the sequent calculus. Cyclic
|
|
proofs is a system of proof search which looks for cycles in a proof tree where
|
|
recursion leads to infinite growth of its branches. It would allow us to avoid
|
|
explicitly using co-induction and thus simplify the description of the
|
|
subtyping relation substantially.
|
|
|
|
|
|
## Cyclic proofs summarized
|
|
|
|
A pre-proof tree is made up of nodes representing the sequents and
|
|
edges corresponding to the pairing of a premise with the conclusion of the
|
|
proof rules used to derive it.
|
|
|
|
In an infinite pre-proof tree there might be cycles. These are paths along
|
|
which equivalent nodes repeat infinitely often. If we are able to identify such
|
|
a path, and the proof makes "progress" each round of the cycle, we can admiss
|
|
it as a proof. If this can be done for all infinite paths, the pre-proof tree
|
|
admissable as an actual proof tree.
|
|
|
|
|
|
In order to use this strategy to decide our subtyping relation, we need:
|
|
* Proof rules
|
|
* Proof tree cycle detection
|
|
* Admissability check, i.e. does the cycle make progress.
|
|
|
|
See here for more info:
|
|
|
|
[fxpl/ln notes on cyclic
|
|
proofs][github.com/fxpl/ln/blob/main/sequel/papper/notes/cyclic-proofs.md]
|
|
|