1.5 KiB
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]
- [slides on cyclic proofs, part 1][ http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part1.pdf ]
- [slides on cyclic proofs, part 2][ http://www0.cs.ucl.ac.uk/staff/J.Brotherston/slides/PARIS_FLoC_07_18_part2.pdf ]