[isabelle] Atb.: Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont



http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/logics.pdf Chapter 4 is almost good description of Theory Sequents (Sequents.thy). From this chapter I finally understood that "real world" sequences (e.g. A) are represented by the lambda term (e.g. %s.Seq0'(A, s). That is fine. Now I can go forward.

Now I am trying to understand:

nonterminal seq and seqobj and seqcont

syntax
 "_SeqEmp"         :: seq                                  ("")
 "_SeqApp"         :: "[seqobj,seqcont] â seq"            ("__")

Isar reference manual (chapter 8) says that nonterminals add additional syntactic categories. Let it be so. But I can not understant the syntax secion. Isar reference manual is saying that syntax secion defines production. But from the other hand the formal secification of the syntax section says, that entries in the syntax sections are in the form:
          Name :: Type (mixfix)
So - how can I interpret such construction as the production? There in this production I can see nonterminals and the relevant string of terminals/nonterminals?

And, of course, I am still seeking the real world interpretation of the nonterminals seq / seqobj / seqcont.

Alex


________________________________
No: Alex Meyer
NosÅtÄts: pirmdiena, 2017. gada 21. augusts 10:32
Kam: cl-isabelle-users at lists.cam.ac.uk
TÄma: Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont


Hello!


I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html and I have problems with the understanding the meaning of the basic items, namely:

types o, seq'

nonterminals seq, seqobj, seqcont?


Do these types and nonterminals have some "real world" counterparts? Sequent is represented by function [o, seq']=>seq', so, maybe o and seq' do not have any real world counterparts?


I am reading "Isabelle's Logics" (especially chapter 4), LNCS 828, Isabelle/Isar reference manual (especially 8.2 and 8.5 about mixfix notations and syntax definition), but I can not grasp the meaning of those symbols and therefor I can not move forward. Any guidance would be very helpful!


I am trying to implement monoidal logic http://www.sciencedirect.com/science/article/pii/S1570868314000573 as a object logic in Isabelle/HOL, but everything is so detached from the "real world" (how the mathematics is being done on paper).




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.