Comment by mafribe | Hacker News Reader

Comment by mafribe | Hacker News Reader

Parent Full thread

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.p...

[2] https://nms.kcl.ac.uk/christian.urban/Nominal

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?

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.

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

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.

Reply on news.ycombinator.com