The paper describing the work in examples/logic/ltl will appear at ITP this
year. Because there's a slight CakeML angle to it, it's available from
cakeml.org at https://cakeml.org/itp18.pdf.
You are right that this work could be described as a deep embedding.
Deep embeddings usually have the advantage that you can describe algorithms on
the syntax, and not just have to think about the semantic values. For example,
you can describe the NNF transformation when you have a deep embedding, but the
best option for something similar with a shallow embedding is a statement of
some equivalences between different semantic formulations of the same thing.
It's also obviously useful to have a type corresponding to the syntax if you
are going to define computable functions to traverse over it and transform it
into automata (as is done in our work).
Michael
On 19/5/18, 00:42, "Chun Tian" <binghe.l...@gmail.com> wrote:
Hi,
I saw how the new LTL formalization (in `examples/logic/ltl`) by Simon
Jantsch suddenly appeared in the past months and because more and more complete
also with help of HOL maintainers. But there’s already an older LTL
formalization (in `src/temporal`) since long time ago, done by Klaus Schneider
et al. [1]
My first question: is there a paper (in PDF, published or unpublished)
documenting the work in `examples/logic/ltl` so that I can learn beside looking
at raw HOL scripts?
Second question: regarding the difference between two versions of LTL
formalizations, can I say the work in `examples/logic/ltl` is a *deep*
embedding? (because it has to define the LTL syntax by a datatype:
val _ = Datatype`
ltl_frml
= VAR 'a
| N_VAR 'a
| DISJ ltl_frml ltl_frml
| CONJ ltl_frml ltl_frml
| X ltl_frml
| U ltl_frml ltl_frml
| R ltl_frml ltl_frml`;
)
while the work in `src/temporal` is *shallow* embedding? (because it
embeds LTL term into HOL as ``:num -> bool`` without using any datatype)
and if so, what’s the pros and cons for choosing one of them as a
working basis (for proving further results)?
Third question: is there a way to connect the two versions of LTL, so that
LTL theorems proved from one side can be (somehow) automatically translated
into theorems on the other side?
Regards,
Chun
[1] Schneider, K., Hoffmann, D.W.: A HOL Conversion for Translating Linear
Time Temporal Logic to ω-Automata. In: Bassiliades, N., Gottlob, G., Sadri, F.,
Paschke, A., and Roman, D. (eds.) LNCS 9202 - Rule Technologies: Foundations,
Tools, and Applications. pp. 255–272. Springer Berlin Heidelberg, Berlin,
Heidelberg (1999).
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
