Stream: Coq users

Topic: Shallow embedding woes


view this post on Zulip towokit928 (May 16 2024 at 02:24):

I shallowly embedded my logic (representing formulae as state -> Prop) and now want to prove determinism of the semantics, but can't do induction on the structure of formulae. Am I out of luck?

Do people do things like maintain a correspondence between deep and shallow representations of the same theory, and switch between them as needed, e.g. with reflection?

view this post on Zulip Johannes Hostert (May 16 2024 at 09:03):

if you want your logic to be deterministic, you might need to restrict the formulas to be "deterministic state -> Props"?

But I'm also not sure what you mean by deterministic in this context?

view this post on Zulip Joomy Korkut (May 16 2024 at 12:46):

You might find this relevant: https://lemonidas.github.io/pdf/DeeperShallowEmbeddings.pdf

view this post on Zulip Pierre Courtieu (May 16 2024 at 13:10):

You need to be a bit more precise about your type of formula vs the semantic. Is state -> Prop the definition of a formula or the type of the interpretation of a formula?

view this post on Zulip towokit928 (May 17 2024 at 02:17):

But I'm also not sure what you mean by deterministic in this context?

Sorry for the vagueness. My logic is behavioral, so the model contains an initial and final state (so the representation is really state -> state -> Prop). Determinism would be something like forall s1 s2 s3, F s1 s2 -> F s1 s3 -> s2 = s3.

Anyway, determinism was just an example of a property which requires induction over the structure of F, which I can't do with this representation (since F s1 s2 is a Prop).

Deeper Shallow Embeddings

I will take a look at this paper, thank you.

Is state -> Prop the definition of a formula or the type of the interpretation of a formula?

As I understand, it's both. It's an assertion like this. That's what I meant by shallow embedding.

I'm considering switching to an inductive type formula to represent the syntax, and a function formula -> Prop to give the interpretation (what I understand as deep), so I can do induction over the structure of the syntax.

view this post on Zulip k32 (May 19 2024 at 08:56):

del


Last updated: Jun 22 2024 at 15:01 UTC