[isabelle] Atb.: Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- To: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Atb.: Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- From: Alex Meyer <alex153 at outlook.lv>
- Date: Wed, 23 Aug 2017 20:39:34 +0000
- Accept-language: lv-LV, en-US
- Authentication-results: outlook.lv; dkim=none (message not signed) header.d=none; outlook.lv; dmarc=none action=none header.from=outlook.lv;
- Cc: Alex Meyer <alex153 at outlook.lv>
- In-reply-to: <HE1P192MB0170271A2B79B29A93411FFA80870@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>
- References: <HE1P192MB017011B3BCED7031CD3B10DC80860@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>, <HE1P192MB0170271A2B79B29A93411FFA80870@HE1P192MB0170.EURP192.PROD.OUTLOOK.COM>
- Spamdiagnosticmetadata: NSPM
- Spamdiagnosticoutput: 1:99
- Thread-index: AQHTGe3RWPFp6WtXPE2Tcxb/e2XAzKKOa0ZbgAJj4Sk=
- Thread-topic: 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
"_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.
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
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).
- Previous by Date: Re: [isabelle] Isabelle2017-RC0: jEdit plugin insists all files for all sessions are present
- Next by Date: Re: [isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- Previous by Thread: [isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
- Next by Thread: Re: [isabelle] Sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont
Cl-isabelle-users August 2017 archives indexes sorted by: [ thread ]
[ subject ]
[ author ]
[ date ]
Cl-isabelle-users list archive Table of Contents
More information about the Cl-isabelle-users mailing list
This archive was generated by a fusion of
Pipermail (Mailman edition) and