Email Gateway (Aug 22 2022 at 15:55): Email Gateway (Aug 22 2022 at 15:55):From: Alex Meyer <alex153@outlook.lv>
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@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).
Last updated: Nov 21 2024 at 12:39 UTC