Stream: Hierarchy Builder devs & users

Topic: Indexed carriers?


view this post on Zulip Shea Levy (Oct 09 2020 at 11:57):

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 (v:x),P(v)\forall (v : x), P(v) but not terms like P(P)P(P) or even (v:y),P(v)\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?

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:00):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:02):

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.

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:03):

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

view this post on Zulip Shea Levy (Oct 09 2020 at 12:04):

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

view this post on Zulip Shea Levy (Oct 09 2020 at 12:05):

Paolo Giarrusso said:

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.

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:05):

do you need to do induction on syntax?

view this post on Zulip Shea Levy (Oct 09 2020 at 12:06):

Can you give an example?

view this post on Zulip Shea Levy (Oct 09 2020 at 12:07):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:07):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:08):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:09):

And using a hierarchy here sounds odd.

view this post on Zulip Shea Levy (Oct 09 2020 at 12:10):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:12):

Not sure how recursion schemes are relevant here.

view this post on Zulip Shea Levy (Oct 09 2020 at 12:12):

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

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:13):

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?

view this post on Zulip Shea Levy (Oct 09 2020 at 12:13):

Yeah

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:13):

The think I do not get, is the indexed part

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:14):

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

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:14):

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.

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:14):

Paolo Giarrusso said:

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

Induction could be an axiom

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:16):

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

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:16):

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

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:16):

Yep, there is a problem indeed

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:16):

that’s a nice way to put it indeed

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:16):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:17):

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

view this post on Zulip Cyril Cohen (Oct 09 2020 at 12:19):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:20):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:21):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:24):

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)

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:24):

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.

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:26):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 12:30):

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.

view this post on Zulip Shea Levy (Oct 09 2020 at 12:44):

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

view this post on Zulip Christian Doczkal (Oct 09 2020 at 12:55):

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.

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 16:49):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 16:50):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 16:51):

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

view this post on Zulip Paolo Giarrusso (Oct 09 2020 at 16:52):

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: Jan 29 2023 at 16:02 UTC