## Stream: Coq users

### Topic: Shallow embedding woes

#### 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?

#### 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 -> Prop`s"?

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

#### Joomy Korkut (May 16 2024 at 12:46):

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

#### 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?

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

#### k32 (May 19 2024 at 08:56):

del

Last updated: Jun 22 2024 at 15:01 UTC