towokit928 (May 16 2024 at 02:24): 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 -> Props"?
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: Oct 13 2024 at 01:02 UTC