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



Sequents, which are lists of formulas, are represented using a trick due to G Huet. The point is to obtain associative unification for free from higher-order unification. Iâm afraid I donât recall many other details: this is 25-year-old work. There are some details in section 3.7 of the Logics manual.

However, not all types need to have "real world interpretationsâ. 

Larry Paulson



> On 23 Aug 2017, at 21:39, Alex Meyer <alex153 at outlook.lv> wrote:
> 
> http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/logics.pdf <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.




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