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?

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?

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

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?

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.

del

Last updated: Jun 22 2024 at 15:01 UTC