I'd like to implement a hierarchy of languages where type indices ensure we have well-formed formulae by construction. E.g. if I have some two-sorted theory and some predicate P over terms of sort x, I'd like to be able to construct terms like $\forall (v : x), P(v)$ but not terms like $P(P)$ or even $\forall (v:y), P(v)$. Can this be done with hierarchy builder? I'm assuming the "carrier" would be an indexed family in this case?

Dear @Shea Levy I am not sure I understand, can you explain what your hierarchy would look like informally?

And are you trying to implement *languages* or their models? For context, when you implement groups, you are implementing *models* of group theory, not the language of group theory.

(Presumably, in algebra you need to formalize the language when dealing with word problems, but that’s the only use case)

Cyril Cohen said:

Dear Shea Levy I am not sure I understand, can you explain what your hierarchy would look like informally?

Could be something like propositional logic, first order logic, first order logic with equality...

Paolo Giarrusso said:

And are you trying to implement

languagesor their models? For context, when you implement groups, you are implementingmodelsof group theory, not the language of group theory.

I'm not completely sure but I think languages. I want to be able to construct formulae, sound arguments given inference rules, etc.

do you need to do induction on syntax?

Can you give an example?

I may want to e.g. reason about proofs or formulae themselves, not just the mathematical objects they represent

`Lemma foo (P : objectProposition) : .... Proof. induction P.`

well, it doesn’t sound like you’re doing algebra, it sounds more like the material in SF . vol 2.

And using a hierarchy here sounds odd.

It's a relationship between the languages though. E.g. the kind of thing I might use recursion schemes for in Haskell

Not sure how recursion schemes are relevant here.

Maybe a red herring. I just want to be able to define languages that have some common syntax/semantics but some extend others.

So I guess the carrier is a type for languages ? The operations would be the constructions of the language (connectives, atoms, etc), and the axioms would be the laws of the logic... Right?

Yeah

The think I do not get, is the indexed part

@Cyril Cohen but having axioms seems not enough, since Shea needs induction on formulas

The way I would implement variable binding would be having a function `fvar : L -> set X`

where `X`

is the parameter holding the type of variables.

Paolo Giarrusso said:

Cyril Cohen but having axioms seems not enough, since Shea needs induction on formulas

~~Induction could be an axiom~~

technically, induction _could_ be an axiom, but then this discussion has a problem

But indeed, by inserting induction as an axiom you are asserting you are dealing with an initial object, and this trivializes each structure and makes inheritance impossible

Yep, there is a problem indeed

that’s a nice way to put it indeed

before discussing implementation details, we should figure out if the mathematics to do is algebra or proof theory.

Algebraic approaches to logic exist, but they look very different — there you’re formalizing Heyting/Boolean algebras

I was focusing on the "indexed" carrier part (because replacing carrier with arbitrary types is indeed a next step for HB)

that certainly has usecases — the obvious formalization of categories uses an indexed/parametric type of arrows?

for the original question by @Shea Levy , I have 2 answers:

1) indexed types might be inappropriate — even if GADTs might be appropriate in Haskell, in Coq they’re often annoying, and you typically rather want separate definitions for “terms” (not-indexed) and “proofs that terms are well-formed” (indexed)

2) it sounds like you want extensible syntax — in Haskell you’d be using “Data types à la carte”. That’s not impossible in Coq (see “meta theory à la carte”), but it’s not worth it.

it’s also not worth it because in proof theory there is often limited reuse when going from a small theory (like propositional logic) to a bigger theory (like FOL).

on answer 1), a needed footnote is that using indexed types “GADT-style” is useful in Agda and has some support in Coq through the Equations plugin. Even then, I’d only recommend that to a pretty small group of specialists, as it’s too easy to paint yourself into a corner that you can’t get out of.

Hmm, OK, thanks! I guess I need to get more clarity on exactly what I'm trying to do

Paolo Giarrusso said:

2) it sounds like you want extensible syntax — in Haskell you’d be using “Data types à la carte”. That’s not impossible in Coq (see “meta theory à la carte”), but it’s not worth it.

Hmm, a while ago I proved soundness and completeness of axiomatizations for Propositional Dynamic Logic (PDL) and PDL with Converse. The diff between the two formalizations is maybe 5% or so, and I would have really liked to have extensible syntax back then, but the paper you mention does not make me eager to look at this more closely. The approach looks really heavy. Still makes me sad though.

@Christian Doczkal I’ve spent significant time on extensible algebraic datatypes/the expression problem — that was not in Coq/Agda but in Scala/Haskell, where more reasonable solutions exist. Therefore, I’d recommend indexing your syntax by a boolean “has_converse” flag, potentially wrapped in a typeclass.

And that’s exactly because a good solution is an open research problem, which I think is really important.

However, supporting arbitrary extensions is much harder than specific extensions (e.g. FOL -> FOL with equality).

While going from propositional logic to FOL seems likely to require starting over and using a different interface, because of binding (disclaimer: I’m actually thinking of STLC -> System F, never actually dealt with FOL)

Last updated: May 28 2023 at 18:29 UTC