-
Notifications
You must be signed in to change notification settings - Fork 9
/
design.mso
227 lines (211 loc) · 26.4 KB
/
design.mso
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
* some design questions to be answered:
1. the object language. can be either stlc+y (finitary PCF), or equivalently HORS, or, using the transfer theorem, have it MSOL just like the type language.
2. MSOL can be augmented with a fragment of counting FOL and remain decidable, while giving the possibility to compare (and add) cardinalities of sets ([2]). need to see how it can fit.
3. need to decide whether MSOL will be used as type language directly, or, an automaton-based typesystem.
//4. need a compositional typesystem (e.g. [3], [9])
4. how can tau support multiple logics?
- a nomic game may take into a consideration additional rules (that may be changed) that speak about "what is truth" and "what amounts as a proof".
- seems like even prolog compiler can be written in MSOL, but need to think how truths/proofs from another logic may be "imported".
- can such tau have only a fragment of full MSOL, and recover even more generalized logics via "trusted compilers"?
- can truth be only something derived from judgements, or we can encode eg "trees of truth"? i think that msol is capable of doing arbitrary Herbrand model reasoning.
5. how good is the idea of using the transfer theorem [23] and be able to use directly only MSOL over [algebraic] graphs? as the terms are regular graphs.
//7. backtracking? ([5])
//8. LISA language (1st order!) [7]
6. in [24] there's *exact* abstract interpretation approach to Ramsay's typesystem. what are the main differences between it and Salvati&Walukiewicz extended scott model? there's at least one similarity, [24] says "To rectify the situation we describe an additional requirement, which is that the abstract property space at ground kind contains “no junk”, and this leads to exact characterisations at higher-kinds." vs [9]'s "Instead our construction introduces ranks only in higher types." (indeed they extend scott model by adding ranks to higher kinds only)
[43], 7. extensions of mso (e.g. [27,29])
8. need to think how logic programming can be decribed as a transition system, especially with constraints-based implementation. [32] presents machine proof for wand(1987) algorithm [35]. [33] is also a very good source for [modern] constraints based [type] inference. it can be a candidate for a level over msol. we could generalize by instead of {spo}=>{spo} have {msol formula} <tranduces to> {msol formula}, where the transduction has to be msol compatible (beyond simply "msol definable"). as subtitutions (courcelle 1998) and evaluation (S&W 2013) are msol compatible, but still need the metalevel flow (e.g. sld resolution). another point to think about here is whether it's possible to allow full second order peano and restrict it when needed to the msol decidable fragment. in any case PA2 can be used on any infinite path, internally, to allow shorter proofs (and contribution of valuable knowledge).
- constraints are sets of equalities and inequalities, namely, a union-find datastructure. how can we express an msol transduction of merging two ufs?
- do introducing fresh variables in the reasoning process is an msol transduction, or only an msol-compatible transduction?
9. can borrow ideas from GP (graph programs) [34]
10. higher order prolog, interesting discussion at [36] and interesting ideas in [37]
11. monadic second order unification as rdf enhancement [38]? or even higher order [39], also cf [40], [41], [42], [43], [45]
12. is stlc(+y?) equiv to higher order set theory over finite universe? [44]. indeed higher order finite set theory is very appealing. cf [46], [47] which has to do with the full msol axiomatization paper [5], also the introduction of bapa is interesting [48] as it shows that BA+MSOL is decidable! (bapa can help understand the limits of decidability of set theories, also recall that ws1s subsumes first order presburger as in eg [19]), new decision procedure for bapa [49].
13. decidablity of quantitative mso [50]
15. yet another mso model [54]
16. decidable mso with cardinality quantifiers [55]
17. very interesting, mso and distributed systems [68]
18. very recent positive result of mso generalization [69]
19. very recent paper by courcelle [70]
20. n3logic (hyperedges replaced by graphs) [71]
21. WSRT, weak second order logic with recursive *datatypes* [75], an extension by MONA:
"This logic corresponds to the core of the FIDO language [16] and is also remi-
niscent of the LISA language [1]. It can be reduced to WS2S and thus provides
no more expressive power, but we will show that a significantly more efficient
decision procedure exists if we bypass WS2S."
22. very important paper about synthesis by kuncak [76]
* relevant information:
1. multiparameter tree transducers [16,17], need to see where completeness is lost there. it also presents a limitation of HORS and tries to overcome it
2. algebraic data structures [18,19,20]
3. verification tool [22]
4. combining different logics: Nelson-Oppen is commonly cited for such. i think that BAMSOL is the choice [48]. enhancements can be found on [53], [58]. -- very good sources! i appreciate kuncak's derivation very much! for his interesting thesis see [60]. cf also [59],[64]. see [61] for another approach. see [62] for another approach by kuncak. [63] for a new thesis regarding theory combination. cf also [67]
5. [65] interesting transfer theorems and about presburger&skolem arithmetics. caucal's hierarchy might be a good basis for logic language design. but cf slide 55 there. see [66] for transfer theorem for generalizations of mso
6. logic programming language for finite sets [72], [73], [74]
* first implementation tasks:
1. stlc+y
//2. HORS
2. parity automata //, collapsible pushdown automata(, ordered tree pushdown)
3. bohm trees
4. krivine machine
//6. transfer theorem
//7. parity games
//8. logical reflection and effective selection ([6])
//9. economical stlc+y <=> HORS ([1])
//10. stlc+y => CPDA ([1])
5. lattice theoretic model of stlc+y under parity automata (conclusion 1 below)
remarks:
1. very fast algorithms can be found at [8]
2. linear dependent types for pcf [15]
3. uncountable quantifier in msol as conservative extention [50]
* food for thought:
1. labels -> equivalences -> prefix orders -> trees
2. every infinite path gives rise to peano arithmetic (might be useful for short and fast proofs)
3. one of the big questions: which logics can msol prove to be consistent? can it prove [in]consistency of any herbrand model? cf [8] p. 149 also can do it in translation to constraints fashion (which is preferrable from runtime complexity point of view) similarly to Wand 1987. also self-verifying systems are very appealing http://www.cs.albany.edu/~dew/m/jsl1.pdf
4. how exactly abstract interpretations and higher order model checking are related? can they benefit from each other? what is the preferred underlying representation, should Galois connections be considered as such?
5. higher order tree functions with (generalized) fixpoint (relaxing the complete lattice structure)?
6. what [25] has to do with all of that?
* "The idea is that such an impasse can be avoided by sharing common subterms along the evaluation process, in order to keep the representation of the output compact, i.e. polynomially related to the number of evaluation steps. But is appropriately managed sharing enough? The answer is positive, at least for certain restricted forms of reduction: the number of steps is already known to be an invariant cost model for weak reduction [BG95, SGM02, DLM08, DLM12] and for head reduction [ADL12]." which affirms that the optimizations in [8] and the ones i developed for sharing trees indeed avoid exponential explosion. krivine machines are about weak head normal form
7. #P problems are also FPT [28]
some conclusions:
1. from the above mentioned options, looks like the model theoretic approach is the best available way. it subsums model checking, transfer theorem, and many more. it was first pioneered in [9], also presented in the very good document [10]. a different model was given in [11, 12 chapter 10]. another different one for wmso in [13], and another fragment (omega-blind) in [14].
2. since we prefer the proof search method for various reasons, the order theoretic models can be seen as a subsystem of [5] (which itself a subsystem of second order peano).
3. querying databanks with msol [56]
4. hors or graphs: cf [93], a graph generalization of Ong 2006. also cf the very good [94]. safety property has strong connection with rules of changing the rules, and modal mu calculus is very interesting to consider. moreover, maybe mso over cpda unfolding is equiv to second order arithmetic.
* references:
[1] "Simply typed fixpoint calculus and collapsible pushdown automata" Salvati&Walukiewicz
[2] https://arxiv.org/abs/1505.06622
[3] www.kb.is.s.u-tokyo.ac.jp/~tsukada/papers/effect-arena-long.pdf
[4] "Recursion Schemes and Logical Reflection" Broadbent, Carayol, Ong, Serre
[5] http://www.anupamdas.com/items/CompAxMSOTrees/CompAxMSOTrees.pdf
[6] https://hal.archives-ouvertes.fr/hal-00865682v2/document
[7] https://swt.informatik.uni-freiburg.de/berit/papers/lisa_a_specification_language_based_on_ws_s.pdf
[8] http://www.di.ens.fr/~mauborgn/publi/t.pdf
[9] https://hal.archives-ouvertes.fr/hal-01145494/document
[10] https://hal.archives-ouvertes.fr/tel-01253426/document
[11] https://arxiv.org/pdf/1502.05147.pdf
[12] https://hal.archives-ouvertes.fr/tel-01311150/document
[13] http://drops.dagstuhl.de/opus/volltexte/2016/6551/pdf/LIPIcs-CSL-2016-11.pdf
[14] https://hal.archives-ouvertes.fr/hal-01169352/file/hal-version.pdf
[15] https://arxiv.org/pdf/1104.0193.pdf
[16] https://pdfs.semanticscholar.org/2853/c0152f9c9abb90d4deefe83e968807e48940.pdf
[17] "High Level Tree Transducers and Iterated Pushdown Tree Transducers" Engelfriet&Vogler
[18] http://www.cs.tsukuba.ac.jp/~uhiro/papers/aplas2010cf.pdf
[19] http://www.brics.dk/mona/mona14.pdf
[20] https://www.cs.ox.ac.uk/files/3721/main.pdf
[21] https://www.react.uni-saarland.de/teaching/automata-games-verification-08/lecture-notes.html good explanations about parity automata
[22] http://spinroot.com/spin/whatispin.html
[23] http://drops.dagstuhl.de/opus/volltexte/2013/4365/pdf/6.pdf
[24] https://www2.warwick.ac.uk/fac/sci/dcs/people/steven_ramsay/dissertation.pdf
[25] https://arxiv.org/pdf/1601.01233.pdf
[26] http://drops.dagstuhl.de/opus/volltexte/2013/4364/pdf/5.pdf
[27] http://drops.dagstuhl.de/opus/volltexte/2015/5430/pdf/27.pdf
[28] http://www.dbai.tuwien.ac.at/proj/tractability/JaklPRW08b.pdf
[29] http://www.math.helsinki.fi/logic/people/hannu.niemisto/MonadicCH.pdf
[30] http://www.dbai.tuwien.ac.at/research/project/tractability/toclGottlobPW10.pdf
[31] https://www.cs.ox.ac.uk/files/1246/bry-rdflog-full.pdf
[32] http://www.cs.uwyo.edu/~jlc/papers/WMM09.pdf
[33] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.710.5020&rep=rep1&type=pdf
[34] https://arxiv.org/pdf/1609.03643.pdf
[35] http://web.cs.ucla.edu/~palsberg/course/cs239/reading/wand87.pdf
[36] http://aitopics.org/sites/default/files/classic/Machine_Intelligence_10/MI10-Ch22-Warren.pdf
[37] https://www.csee.umbc.edu/courses/771/papers/mu_96_02.pdf
[38] http://www.iiia.csic.es/~levy/papers/1190.pdf
[39] https://www4.in.tum.de/publ/papers/Prehofer-CADE1994.pdf
[40] https://www.lix.polytechnique.fr/~dale/papers/Handbook_Logic_AI_LP.pdf
[41] http://www.lix.polytechnique.fr/~dale/papers/iclp88.pdf
[42] http://gpd.sip.ucm.es/uploads/pdf/LiptonNieva-tlca07_LiptonNievaTLCA07.pdf
[43] http://ac.els-cdn.com/S0890540197926948/1-s2.0-S0890540197926948-main.pdf?_tid=ce7ebc58-9a43-11e6-86e1-00000aab0f01&acdnat=1477352857_e73f208c83d79454595c840dedecd7d5
[44] www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-9.rr.ps
[45] http://gpd.sip.ucm.es/uploads/pdf/LiptonNieva-tlca07_LiptonNievaTLCA07.pdf
[46] https://www.dimi.uniud.it/~dovier/PAPERS/jlpsetlog.ps.gz
[47] http://www.cs.yale.edu/homes/piskac/publications/WiesPiskacKuncak09CombiningTheories.pdf
[48] https://arxiv.org/pdf/cs/0407045.pdf
[49] http://homepage.divms.uiowa.edu/~ajreynol/ijcar16b.pdf
[50] http://www.cs.ox.ac.uk/people/vince.barany/msoc_trees_FI.pdf
[51] https://www.cs.ox.ac.uk/people/cristian.riveros/papers/lics13.pdf
[52] http://www.brics.dk/mona/papers/mona-decidable-arithmetic/draft.pdf
[53] http://arw.csc.liv.ac.uk/year/2014/ARW2014proceedings.pdf#page=8
[54] https://arxiv.org/pdf/1503.08936v2.pdf
[55] https://logic.rwth-aachen.de/~kaiser/msoc_chains.pdf
[56] http://www.tcl-sfs.uni-tuebingen.de/MonaSearch/monasearch-submission.pdf
[57] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.83.261&rep=rep1&type=pdf
[58] http://lara.epfl.ch/~kuncak/papers/KuncakETAL05AlgorithmDecidingBAPA.pdf
[59] https://arxiv.org/pdf/0801.2498.pdf
[60] http://icwww.epfl.ch/~kuncak/papers/Kuncak07DecisionProceduresModularDataStructureVerification.pdf
[61] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.76.6150&rep=rep1&type=pdf
[62] https://infoscience.epfl.ch/record/133549/files/main.pdf
[63] http://pubs.doc.ic.ac.uk/cooperative-program-verifiers/cooperative-program-verifiers.pdf
[64] https://userpages.uni-koblenz.de/~mbender/sum_full.pdf
[65] http://bc12.labri.fr/slides/igw.pdf
[66] http://www.cs.ox.ac.uk/stephan.kreutzer/Publications/05-jlc.pdf
[67] http://www.fi.muni.cz/~blumens/Publications/Operations.pdf
[68] http://www.lsv.ens-cachan.fr/~bollig/MPRI/non-sequential.pdf
[69] https://pdfs.semanticscholar.org/e78c/2a0ee2c418211c45f88f2f9520d8a81f6d4b.pdf
[70] https://hal.archives-ouvertes.fr/hal-01299077/document
[71] https://www.uni-oldenburg.de/fileadmin/user_upload/informatik/radthe16_21.06.16.pdf
[72] www.sciencedirect.com/science/article/pii/0743106695001476
[73] https://users.dimi.uniud.it/~agostino.dovier/PAPERS/tesi_1mar96.pdf
[74] https://arxiv.org/pdf/cs/0309045.pdf
[75] http://www.brics.dk/mona/papers/c-trees/paper.pdf
[76] http://www.cs.yale.edu/homes/piskac/publications/KuncakETAL10CompleteFunctionalSynthesis.pdf
[77] http://math.andrej.com/wp-content/uploads/2016/01/self-interpreter-for-T.pdf
[78] http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/PCF.pdf
[79] "Fundumental properties of infinite trees" Courcelle 1983 http://www.diku.dk/hjemmesider/ansatte/henglein/papers/courcelle1983.pdf
[80] http://www.labri.fr/perso/courcell/ArticlesEnCours/RegMSOquasiTrees.pdf
[81] https://people.math.osu.edu/lang.162/book/NaiSo1.pdf analytic treatment of trees, also in [80] but this one is in a mathematical physics journal (and is about hilbert spaces). for rkhs over trees:
[82] http://users.cecs.anu.edu.au/~williams/papers/P175.pdf extremely interesting see even:
[83] https://en.wikipedia.org/wiki/Tree_kernel cf also
[84] http://jmlr.csail.mit.edu/papers/volume11/vishwanathan10a/vishwanathan10a.pdf
[85] http://disi.unitn.it/moschitti/Tree-Kernel.htm (svmlight)
[86] http://www.jaist.ac.jp/~mizuhito/papers/conference/CADE05.pdf a paper by satoshi about verifying merkle tree algorithm with msol over trees (MONA)
[87] http://software.imdea.org/~mauborgn/publi/esop00.pdf sharing trees (tree schemata?) in short paper (rather that thesis). interestingly his algo has some kind of optimality
[88] http://rho.loria.fr/data/rhoSN.pdf formalization of pattern matching in lambda calculus
[89] https://www.cl.cam.ac.uk/~mom22/jit/jit.pdf can this be formalized as stlc+y self interpreter?
[90] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.105.96&rep=rep1&type=pdf language for xml based directly on msol
[91] http://www.ti.inf.uni-due.de/publications/koenig/icgt08b.pdf recognizability in category theory, interesting
[92] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.43.7489&rep=rep1&type=ps poset-centric treatment
[93] http://www.cs.rhul.ac.uk/home/hague/files/papers/lics08b-long.pdf
[94] http://william.famille-blum.org/research/thesis-submitted.pdf
[95] http://www.cs.ox.ac.uk/andrew.ker/docs/ADK02C.pdf what about trees genrated by untyped lambda calculus? see here
[96] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.46.2257&rep=rep1&type=pdf nice paper about nomic. another one is:
[97] http://www.egov.ufsc.br/portal/sites/default/files/anexos/2901-2895-1-PB.pdf
[98] http://www.estrellaproject.org/
[99] http://www.aclweb.org/anthology/W13-1811 a deep connection between rdf and msol
[100] http://informatique.umons.ac.be/tcs/Francqui/slides/mons2b.pdf yet another first class review by Wolfgang Thomas. includes a predicate for being a power of two.
[101] https://arxiv.org/pdf/1608.00653v1.pdf interesting generalized decidability result for synthesis. as usual, quoting interesting theorems.
[102] http://www-sop.inria.fr/members/Joelle.Despeyroux/papers/types98.ps interesting conservative extention to stlc
[103] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.568&rep=rep1&type=pdf very nice source about self-modifying protocols
[104] http://www.cs.bham.ac.uk/~ohf162/icfp14.pdf distributed [rpc] krivine machine
[105] http://math.andrej.com/2009/03/21/how-to-simulate-booleans-in-simply-typed-lambda-calculus/
[106] https://proglang.informatik.uni-freiburg.de/teaching/konzepte/2015/20150601-note.pdf proof that pcf can interpret system t
[107] https://arxiv.org/pdf/1511.02629.pdf finally computing normal form without substitutions trouble. there's another good source for this subject which i dont recall now
[108] https://www.itu.dk/~sestoft/pebook/jonesgomardsestoft-letter.pdf how to write specializers
[109] http://meta2016.pereslavl.ru/papers/2016_Berezun_Jones__Working_Notes__Compiling_ULC_to_Lower-level_Co_de_by_Game_Semantics_and_Partial_Evaluation.pdf contiuation of the work in [107]
[110] http://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/hosc-fpcd.pdf very close to my conjecture from taylor series / cumulants of bool funcs, that higher order funcs (specifically, equality) can give optimal compression. also gives rise to optimal storage for reasoner. everything is a tree after all (cf esp the pattern matching part in the paper). interestingly the paper uses intersection types. indeed the typesys presented there is very interesting.
[111] Theorem 3. A λ-term M is typable in CDV iff M is strongly normalizable. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.378.6306&rep=rep1&type=pdf
[112] http://www-kb.is.s.u-tokyo.ac.jp/~koba/papers/popl2017-long.pdf new paper from today: reduction from a kind of higher order logic to mso-equiv (modal mu) and vice versa. impliying corresponding decidability results. in p11 demonstrate how to count with hors. indeed all very similar to ackerman coding. is it as optimal?
[113] http://www2016.net/proceedings/proceedings/p263.pdf json in mso
RDF setting:
a kb consists of a set of rdf graphs, each contains rules. every graph can be written as a tree where the root's decendants are the rules, where each rule has two subtrees (premises and consequences) that consist of triples and from here we have the usual tree-term structure. the tree is labeled by two labels: context and uri, to be expressed via two equivalence relations among tree nodes and across graphs.
we want to be able to assert MSOL properties on this tree. in addition, we'd like to use a tree generator that supports much larger class of MSOL definable trees (yet MSOL decidable), namely, trees generated by higher order recursion schemes. plain rdf graphs seem to be a first order recursion scheme.
we would therefore be interested in incorporating a typesystem into rdf (via the predicate rdf:type or just "a" in short) that speaks about those trees and express MSOL formulas about them. basically we have two kinds of trees to model-check: those who consist of rdf resources (uris), and those who consist of triples (graphs), where obviously the formers are subtrees of the latters.
since on this setting all rdf resources are tree nodes, the typesystem can quantify over sets of such.
a rule is ground if it's given without any premise nor free variables, or if all its premises are ground under certain equivalence (which are actually substitutions but significantly simplified). specifically, the rules themselves determine the allowed substitution together with few more metarules.
the semantics of an rdf graph is very similar to lambdas' Bohm tree. for a convenient typesystem we'll have to see whether rdf graph entailment is msol expressible. it seems easy on first order setting, but can it be done with higher order recursion scheme? it seems like it's possible with having n+1 order scheme. it's better to do it with msol but ofc stlc+y is as good. -- cf http://www.labri.fr/perso/salvati/downloads/presentations/Main.pdf pdf page 109
a proof is a tree with root being the query. a node may have k successors where k is the number of rules, giving rise to (W)SkS such that the k successors are distinguished from each other. indeed, each rule encapsulate a different unification predicate. if match occurs, this rules have successors which represent its premises to be grounded, giving another set of successors. so the total number of different successor relations is bounded by the number of heads plus the number of premises. the match predicates consist of expressing whether certain equivalences can be declared without breaking the metarules (of tree structure, equivalence relations and unification). so the proof tree is msol expressible with WSkS and k rules (aside the metarules), each contribute another two levels to the proof tree in every iteration over the leaves. iterating over all possible equivalences (substitutions) is exactly where monadic second order comes in (set variables). if we use SkS rather WSkS, we can even speak about infinitely many variables. this reminds the transfer theorem from [23] which allows infinitely many Y variables but not lambda variables.
enhancing rdf to higher order recursion schemes require the ability for a kb to speak about its own rules, and moreover, to quantify rules (strongly connected to nomic), and to have rules that accept rules as parameters and return rules. an n-order recursion scheme would have rules-over-rules-over-... to height n. an rdf rule can be seen as a graph by its own, as it's essentially a triple with log:implies and two graph identifiers, and a single triple can be seen as a graph by its own. indeed in the rdf-to-tree representation we began with, equivalence can be done among resources and graph nodes as well. an "ordinary" rdf graph is aware only to the lower levels of this tree, namely, the triples themselves, but not to the upper levels (graphs and rules). we can therefore go up from a definition of graph to a definition of the whole kb, and let the kb itself be aware to it's whole structure. specifically it means that the whole kb tree described above will be accessed from some enhanced syntax, or using builtins. then, we are able to speak about rules directly, or even specify rules implicitly, namely, we got higher order recursion scheme.
as in [23], stlc+y representing a bohm tree can itself be a regular tree, and even finite. only the bohm tree can be infinite and irregular on this setting. it's interesting that our description of msol-definable resolution does not go through the bohm tree, namely the semantics of the rdf kb, but performs the backtracking on the syntactic level only. reasoning over graphs' bohm trees would be another feature, much more powerful than offered in total languages where the bohm tree is always finite, and here is not even msol expressible (yet msol decidable) as it's always context-sensitive. but one could argue that we still lose nothing by keeping it msol definable graphs: the transfer theorem show that properties of bohm trees are properties of regular term graphs. so bohm trees can be reasoned over but in a way that does not essentially increase the expressibility of such enhanced rdf graphs. in fact, by adding more axioms for internal use (e.g. PA2), the transfer itself may be performed by means of proof search.
a set of rdf quads is nothing but a way to define labelled graphs. an rdf kb+query is a tree grammar as it represents the sets of all valid proof trees. the proof tree is very closely related to bohm trees, and indeed logic programming is about inference being beta reduction. if P(x)=>Q(x) is a logic program clause, where P,Q are some predicates and (boldface) x is a tuple of variables, then we can write it as a recursion scheme Q(x)=P(x) (we flip the sides since under backtracking semantics of logic programs, Q calls P). it is a 1st order recursion scheme if we name all rules (or taking the predicate as the name in case we disallow predvars), and call all of them in every predicate. this (hors) seem to be a more suitable representation than stlc+y (yet they're equivalent as proved recently [26]) for logic programs.
the monadic datalog parallel [30] might give plenty of ideas for rdf, also [31] shows that this solves some puzzles with blank nodes.
every (finite) AST can uniquely be described by an MSOL formula, with two successors and two eqrels (for rdf).
some plan:
have bamsol with max/min enhancements. programs will be represented by stlc+y trees (as in "evaluation is msol compatible" paper) with keeping the transfer theorem in mind (i.e. nonregular trees and the transfer itself). it seems like there is a way to reduce bamsol to [exponentially large] presburger. this in turn can be solved more efficiently with second order peano.
tau is really a so-called "filtration", namely, a process over time where the past partly determines the future. On every tick we have an amendment A which takes every rule R and transforms it into new rule R(n) = A(n, R(n-1)).
rules form a tree (hors) or graph, and an msol definable or compatible transduction is the transition between blocks, or, amendments. the code of the client is then synthesized from the graph, making use of the corresponding transfer theorems. so a block contains an msol compatible transduction, beginning with the "empty" tree.
constraining the next block has to be done in the tree (stlc+y) level, namely the stlc+y code will have to know to do the transfer operator. the transfer operator can be enfored on the ast level tree or maybe even in the bohm tree (at least partially). both are msol trees/graphs thanks to the transfer itself (this may give rise to some diagonalization arguments). specifically, if finitary pcf can do transfer from msol<->stlc+y (S&W paper "evaluation is msol compatible"), then...
--- indeed: "We can ask whether Theorem 2.2 can be inverted: does a simply typed λ-calculus
with natural numbers and fixed-point operators have a self-interpreter? As Alex Simpson
ON SELF-INTERPRETERS FOR SYSTEM T AND OTHER TYPED λ-CALCULI 3
pointed out to me, the question was answered affirmatively by John Longley and Gordon
Plotkin who described a rather intricate self-interpreter for PCF [6, Prop. 6]." [77]
see also [78] for pcf self interpreter
... then this means than finitary pcf can do self-evaluation hence transfer to bohm tree,