4 ms·

One example are nominal techniques [1]. While they are constructive, they have so far only found substantial implementation in Isabelle/HOL [2]. The reason is t

One example are nominal techniques [1]. While they are constructive, they have so far only found substantial implementation in Isabelle/HOL [2]. The reason is that the natural implementation is non-constructive, and leads to only a small blowup in proof complexity, which can easily be handled by Isabelle/HOL's proof automation. In contrast, constructive implementations of nominal techniques seem to require a considerable blowup in logical complexity, which the existing proof automation in Curry-Howard based provers doesn't seem to handle gracefully. Another issue is that most of the automation that is known as "hammer" is based on non-constructive automatic provers. [1] https://www.cl.cam.ac.uk/~amp12/papers/nomlfo/nomlfo-draft.pdf https://www.cl.cam.ac.uk/~amp12/papers/nomlfo/nomlfo-draft.p... [2] https://nms.kcl.ac.uk/christian.urban/Nominal https://nms.kcl.ac.uk/christian.urban/Nominal

pacala 9y ago
Is there a motivating example that compares nominal techniques in Isabelle with standard techniques in Coq or Lean over the same simple theorems?
- mafribe 9y ago
  Not that I'm aware of. It would be nice to have one. The number of people who understand nominal, HOL, CoC and implementations of provers is vanishingly small.
fmap 9y ago
Do you know why that is the case? Nominal logic is usually presented as a sheaf model (i.e., as the internal language of the Schanuel topos), which models a constructive dependent type theory. Is there a problem when constructing a universe?
- mafribe 9y ago
  I'm probably the wrong person to discuss this question with. I don't know more than I've written above. All I know about this is from conversations with Christian Urban, who implemented Nominal Isabelle. It was a while back, maybe the problem of implementing nominal techniques in constructive type theory in an effective way (i.e. doesn't put additional burden on automation) has been solved by now. The problem as I understand it is this. Let's say you have a theory T in the formal language given by signature S. - In HOL you extend T to T' and S to S', but the deltas between T and T', and S and S' are small, and largely generic. This is possible because almost everything handling nominal can be done using double negation. - In CoC you extend T to T' and S to S', but the deltas between T and T', and S and S' are huge, and largely non generic.

pacala 9y ago

Is there a motivating example that compares nominal techniques in Isabelle with standard techniques in Coq or Lean over the same simple theorems?

mafribe 9y ago
Not that I'm aware of. It would be nice to have one. The number of people who understand nominal, HOL, CoC and implementations of provers is vanishingly small.

fmap 9y ago

Do you know why that is the case? Nominal logic is usually presented as a sheaf model (i.e., as the internal language of the Schanuel topos), which models a constructive dependent type theory. Is there a problem when constructing a universe?

mafribe 9y ago
I'm probably the wrong person to discuss this question with. I don't know more than I've written above. All I know about this is from conversations with Christian Urban, who implemented Nominal Isabelle. It was a while back, maybe the problem of implementing nominal techniques in constructive type theory in an effective way (i.e. doesn't put additional burden on automation) has been solved by now. The problem as I understand it is this. Let's say you have a theory T in the formal language given by signature S. - In HOL you extend T to T' and S to S', but the deltas between T and T', and S and S' are small, and largely generic. This is possible because almost everything handling nominal can be done using double negation. - In CoC you extend T to T' and S to S', but the deltas between T and T', and S and S' are huge, and largely non generic.