Hi Michael, thanks for the explanation and paper link!
Regards, Chun > Il giorno 20 mag 2018, alle ore 11:56, michael.norr...@data61.csiro.au ha > scritto: > > 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
signature.asc
Description: Message signed with OpenPGP
------------------------------------------------------------------------------ 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
