4 ms·

It's important to sometimes step back and think about whether what you are doing actually makes sense. There are some assumptions about how formal logic is done

It's important to sometimes step back and think about whether what you are doing actually makes sense. There are some assumptions about how formal logic is done in ITP (interactive theorem proving) systems that should be challenged. Here is my opinion about that: https://doi.org/10.47757/practal.1 https://doi.org/10.47757/practal.1

cjfd 5y ago
What you state about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master/fusion.ml https://github.com/jrh13/hol-light/blob/master/fusion.ml lines 600-637. Coq has sig in the standard library which is not quite it but becomes a lot closer when one assumes proof irrelevance. Also, a COC-based prover can easily be given subsets with a few easy axioms. Your point that currently it is quite hard to do anything practical in all of the interactive theorem provers is very true, though.
- practal 5y ago
  I know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily. [1]: https://link.springer.com/chapter/10.1007/11814771_27 https://link.springer.com/chapter/10.1007/11814771_27
- momentoftop 5y ago
  HOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of the other. So, in a truly subtyped system, you would have it that 3 has both type N and type R, with N being a subtype of R. Instead, in HOL Light, there is a total function from N to R, and a partial function from R to N. HOL Light allows you to carve out new types of existing types using a predicate filter, and this is baked into the kernel in `fusion.ml`. But this doesn't introduce subtyping relations. Importantly, the kernel rule gives you abstraction and representation functions to move between elements of the new type and the original type, but, unlike in a subtyping system, the terms of the newly defined type are not simultaneously elements of the larger type.
ImprobableTruth 5y ago
I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so that I'd suspect starting with 'what you want' has a good chance of making the system unworkable due to breaking something like computationality or making classical logic unsound while making it very hard to notice (if it's not a theoretical property, then something more practical could also be problematic. Something like automation isn't a panacea either because a system needs to be amenable to it). Extending existing systems with something like intersection types seems already hard enough. As an example, it's very hard for me to judge what it means for equality to not have a type without an underlying system to go along with it. Since it's still featured as part of types (such as your dom f = A ∧ cod f = B example), you still need a typing rule, but what would that look like? It's at the very least non-obvious to me that this doesn't potentially have some issues. Or, what does extensionality for types cover that isn't done by subtypes? And should this just be a metatheoretic property, or also something that can be stated inside the system? Besides that, the current items on the list are of course reasonable enough (though nil strikes me as a regression from option types and paraconsistent logic strikes me as totally unusable in the general case as you'd lose A \/ B, ~A |- B, which is absolutely essential.)
- practal 5y ago
  You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T]. I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it. With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.
creata 5y ago
> Instead, coercions are used to emulate some of the advantages of subtyping. Maybe I missed it in the article, but what does subtyping give you that coercions don't?
- ImprobableTruth 5y ago
  While I'm not sure it's impossible (though if it's possible I doubt it would be pretty or non-fragile), I've at least never seen anybody emulate generic intersection/union types using coercions. Dependent intersections like in Cedille are definitely impossible.
  - practal 5y ago
    Very good point.
- practal 5y ago
  Economy of thought. In my opinion, subtyping declares a "is" relationship, and coercions declare a "can be viewed as" relationship. You would want both in Practal. Subtyping is more tricky than coercions in the sense that if done wrongly, it can introduce inconsistencies, while coercions cannot (they just may fail to be unique). For example, ℕ should be a subtype of ℝ. Because a natural number IS a real number. Let's say you have the theorem `∀ x : ℝ. P x` for some predicate `P`. With subtyping, also the theorem `P n` holds for any `n : ℕ`. With coercions, only the theorem `P (c n)` holds, where `c : ℕ → ℝ` is the coercion. Now you have an additional constant `c` in your theorem. It makes things more complicated than they have to be. Sure, some pretty printing and nifty automation can help you a lot here, but why would you want to deal with that added coercion tax in the first place for cases where you don't have to?

cjfd 5y ago

What you state about subtypes is not really true. HOL Light has subtypes baked into the kernel of the system. See https://github.com/jrh13/hol-light/blob/master/fusion.ml https://github.com/jrh13/hol-light/blob/master/fusion.ml lines 600-637. Coq has sig in the standard library which is not quite it but becomes a lot closer when one assumes proof irrelevance. Also, a COC-based prover can easily be given subsets with a few easy axioms. Your point that currently it is quite hard to do anything practical in all of the interactive theorem provers is very true, though.

practal 5y ago
I know the kernel of Hol-Light very well, as I implemented proof terms for it [1]. 600-637 do not define subtypes, but entirely new types. And no, you cannot add subtypes to a COC prover easily. [1]: https://link.springer.com/chapter/10.1007/11814771_27 https://link.springer.com/chapter/10.1007/11814771_27
momentoftop 5y ago
HOL Light doesn't have subtyping. If the type system had subtyping, there would be terms that are assigned two different types, where one type is a subtype of the other. So, in a truly subtyped system, you would have it that 3 has both type N and type R, with N being a subtype of R. Instead, in HOL Light, there is a total function from N to R, and a partial function from R to N. HOL Light allows you to carve out new types of existing types using a predicate filter, and this is baked into the kernel in `fusion.ml`. But this doesn't introduce subtyping relations. Importantly, the kernel rule gives you abstraction and representation functions to move between elements of the new type and the original type, but, unlike in a subtyping system, the terms of the newly defined type are not simultaneously elements of the larger type.

ImprobableTruth 5y ago

I'm not convinced that it's feasible to design a language that way because features and the underlying system generally seem to influence each other so much, so that I'd suspect starting with 'what you want' has a good chance of making the system unworkable due to breaking something like computationality or making classical logic unsound while making it very hard to notice (if it's not a theoretical property, then something more practical could also be problematic. Something like automation isn't a panacea either because a system needs to be amenable to it). Extending existing systems with something like intersection types seems already hard enough. As an example, it's very hard for me to judge what it means for equality to not have a type without an underlying system to go along with it. Since it's still featured as part of types (such as your dom f = A ∧ cod f = B example), you still need a typing rule, but what would that look like? It's at the very least non-obvious to me that this doesn't potentially have some issues. Or, what does extensionality for types cover that isn't done by subtypes? And should this just be a metatheoretic property, or also something that can be stated inside the system? Besides that, the current items on the list are of course reasonable enough (though nil strikes me as a regression from option types and paraconsistent logic strikes me as totally unusable in the general case as you'd lose A \/ B, ~A |- B, which is absolutely essential.)

practal 5y ago
You don't need a rule system to understand what equality is. Yes, it is not computational for sure. It's a logic, not a programming language. Nil is the way undefinedness is handled in Practal. It is the most elegant way I can think of. You can still have your option type, just as you can have Kleene logic operators, but these are more suitable for doing program verification work in Practal, not so much for doing general mathematics in Practal. You really want (T ∪ Nil) ∪ Nil = T ∪ Nil here, while in programming you usually don't want Option[Option[T]] to be the same as Option[T]. I am not saying it is easy to make all of this work, and to make it work soundly. But less just doesn't cut it. With a kernel-based approach, you have a chance to get it right. If you find an inconsistency, fix the kernel, and move on. Automation works just on top of it, and doesn't affect soundness. This is the great thing about automation in kernel-based ITP: If it finds some solution or counter-example, great. Otherwise, no harm done.

creata 5y ago

> Instead, coercions are used to emulate some of the advantages of subtyping. Maybe I missed it in the article, but what does subtyping give you that coercions don't?

ImprobableTruth 5y ago
While I'm not sure it's impossible (though if it's possible I doubt it would be pretty or non-fragile), I've at least never seen anybody emulate generic intersection/union types using coercions. Dependent intersections like in Cedille are definitely impossible.
- practal 5y ago
  Very good point.
practal 5y ago
Economy of thought. In my opinion, subtyping declares a "is" relationship, and coercions declare a "can be viewed as" relationship. You would want both in Practal. Subtyping is more tricky than coercions in the sense that if done wrongly, it can introduce inconsistencies, while coercions cannot (they just may fail to be unique). For example, ℕ should be a subtype of ℝ. Because a natural number IS a real number. Let's say you have the theorem `∀ x : ℝ. P x` for some predicate `P`. With subtyping, also the theorem `P n` holds for any `n : ℕ`. With coercions, only the theorem `P (c n)` holds, where `c : ℕ → ℝ` is the coercion. Now you have an additional constant `c` in your theorem. It makes things more complicated than they have to be. Sure, some pretty printing and nifty automation can help you a lot here, but why would you want to deal with that added coercion tax in the first place for cases where you don't have to?