[Merged by Bors] - feat: Ordinal Approximants of the least/greatest fixed point in a complete lattice#8996
[Merged by Bors] - feat: Ordinal Approximants of the least/greatest fixed point in a complete lattice#8996PhoenixIra wants to merge 32 commits intomasterfrom
Conversation
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
Sorry for the delayed response here, @PhoenixIra. I don't know enough about the mathematics to judge whether this is the right thing to prove, but I can make suggestions about mathlib style, which you'll find below. Could you let us know whether you're still up for finishing this PR?
|
Thank you for the detailed comments! I am rather busy the next two weeks. But as soon as I get to it, I will incorporate or react to all comments. I am also still very motivated to finish up the PR. |
|
I believe, I have addressed all issues. Please let me know if I missed anything. |
|
Thank you for the review and don't worry about the delay. I have changed the documentation to only communicate the approximation scheme and explain why it's not constructive (despite the name of the papers). If I missed anything, please let me know. I also decided to remove Ordinal from the filename, as the filename was already very long. Please also let me know if you think this is confusing now (as e.g. the Kleene fixed-point theorem is not located there) I will also resolve / comment on your detailed comments. |
fpvandoorn
left a comment
There was a problem hiding this comment.
Thanks for the changes.
I have a few more suggestions. If you incorporate those (and the same for gfp, then I'm happy to merge this.
|
Can you move/rename the file to |
|
Every suggestion should be incorporated. |
|
Thank you for incorporating all review suggestions! bors merge |
…plete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs. Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
|
Pull request successfully merged into master. Build succeeded: |
…plete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs. Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
…plete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs. Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
…plete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs. Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
…plete lattice (#8996) Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive. This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs. Co-authored-by: Ira Fesefeldt <public@feuervogel.me>
Define ordinal approximants for the least/greatest fixed points of a monotone function in a complete lattice. It is sometimes also called the constructive Knaster-Tarski Theorem, first introduced by Cousot & Cousot in 1979. This implementation is however not constructive.
This has a variety of applications in non standard logics and proofs such as quantitative logics or cyclic proofs.
I am a bit unsure about the placement of certain theorems, namely:
limitationdefinition and its theorems. This feels very special to this theorem. Thus I left it in this file. It could however also live somewhere in Ordinals/Cardinalsmonotone_stabilizingandantitone_stabilizing. I first thought about placing them inMathlib.Order.Monotone.Basic. However,Monotoneis using preorders and not partialorders, where this theorem does not hold. Maybe this theorem is also already proven somewhere else and I missed it?OrdinalApproxnamespace could also live inMathlib.Order.FixedPoints. However, I decided aginst it as this would mean that importingMathlib.Order.FixedPointswould also import a lot of (likely unecessary) files fromMathlib.SetTheory.OrdinalandMathlib.SetTheory.Cardinalwhen not using ordinal approximants.I appreciate comments regarding these questions and reviews in general. I also appreciate a comment if this has already been done and I just totally missed it.