feat(Foundations/Logic): Notation typeclasses and models#582
feat(Foundations/Logic): Notation typeclasses and models#582thomaskwaring wants to merge 2 commits into
Conversation
There was a problem hiding this comment.
General comments:
- Could you remove the prime "'" in this PR branch's name? The prime symbol is a quote for shell and needs to be escaped in shell commands like
git checkout. - Why do many class names contain the word
Class, which seems completely unnecessay?
This is a partial review. More comments will be added later.
| /-- Forcing relation associated to each parameter. -/ | ||
| ForcesAt (b : β) : (Param b) → α → Prop | ||
|
|
||
| scoped notation w " ⊨[" b "] " a => ParamModelClass.ForcesAt b w a |
There was a problem hiding this comment.
I find the order in which the arguments appear in the notation unintuitive: a is a "world" in model b, and yet w appears before b in the notation. Wouldn't it be better to write something like b, w ⊨ a?
| interpretations are considered valid. -/ | ||
| class InterpModelClass (α : outParam (Type*)) (β : Type*) extends HasInterp α β where | ||
| /-- The set of valid interpretations. -/ | ||
| filter (b : β) : Set (Ground b) |
There was a problem hiding this comment.
Rather than Set, perhaps something like CompleteAtomicBooleanAlgebra will provide more generality?
| class AlgebraicAnd (α β : Type*) [HasInterp α β] [HasAnd α] [∀ b : β, Min (Ground b)] where | ||
| interp_and_eq (M : β) (x y : α) : interp M (x ∧ y) = interp M x ⊓ interp M y | ||
|
|
||
| class AlgebraicOr (α β : Type*) [HasInterp α β] [HasOr α] [∀ b : β, Max (Ground b)] where | ||
| interp_or_eq (M : β) (x y : α) : interp M (x ∨ y) = interp M x ⊔ interp M y | ||
|
|
||
| class AlgebraicImpl (α β : Type*) [HasInterp α β] [HasImpl α] [∀ b : β, HImp (Ground b)] where | ||
| interp_impl_eq (M : β) (x y : α) : interp M (x → y) = interp M x ⇨ interp M y | ||
|
|
||
| class AlgebraicNot (α β : Type*) [HasInterp α β] [HasNot α] [∀ b : β, Compl (Ground b)] where | ||
| interp_not_eq (M : β) (x y : α) : interp M (¬ x) = (interp M x)ᶜ |
There was a problem hiding this comment.
I don't understand these definitions. What are those lattice-theoretic operations like ⊓ and ⊔? What sort of algebraic structures do you assume Ground b to have? How are Ground b related to filter b?
| /-- `Forces b a` has the intended semantics "`a` is valid in the model `b`". -/ | ||
| Forces : β → α → Prop | ||
|
|
||
| scoped notation "⊨[" b "] " a => ModelClass.Forces b a |
There was a problem hiding this comment.
Why not write b ⊨ a? See also my comment about the notation for ForcesAt.
|
|
||
| /-- Objects of type `β` carry a forcing relation worlds of type `γ` and the proposition type `α`. -/ | ||
| class ParamModelClass (α : outParam Type*) (β : Type*) where | ||
| Param : β → Type* |
There was a problem hiding this comment.
It is not clear to me why we need this generality. Can you give a natural example of the use of ParamModelClass?
Note also that ParamModelClass can be implemented using ModelClass by substituting a dependent sum type for β, namely, Σ b : β, Param b, which means that the only thing that ParamModelClass gives you is the bundling of Param.
2 participants
A proposal for typeclasses expressing that a type of "propositions" has semantics in a type of "models".
Main definitions
ModelClass α β: objects of typeβcarry a predicateForceson objects of typeα.ParamModelClass α β: objectsM : βcarry a forcing relation parametrised over some auxiliaryParam M : Type*InterpModelClass α β: eachM : βhas an associated ground typeGround M, an interpretationinterp : α → Ground Mand afilter : Set (Ground β), which induces a forcing relation asForces M a := interp a ∈ filter M.I've tried to add enough examples to show how this might be used, but the design ought to be discussed before we settle on anything this general.