thanks,
@Ohad, I have a question. I've skimmed through the IRC logs of the last two months and found a very promising conversation between you, HMC and Stoopkid on 6 June about the maths of the new Tau.
that wasn't about the math of the new tau (as its logic is beyond what mentioned there) but i deliberately didn't want to expose any design detail, so i let the discussion revolve around mso vs mltt. the old vs new tau is already (and was back then 2m ago) light years from that subject
As far as I have been able to understand, HMC and Stoopkid where trying to understand how MSOL is able to verify higher order programs in spite of not being itself a full second order logic.
well they spoke about "higher order logic" without saying what it actually refers to, and this is part of what made the discussions very futile: the order of the logic is only one property of a logic, it by no means tells everything interesting (like expressiveness or decidability) as for itself (but in conjunction with other properties of the logic in concern).
but indeed as you point out, i answered for the scope of verifying higher-order functional programs. and indeed (as below), stlc is higher order (and the Y can make it "infinite order" call it so). so if we got an stlc program we can verify it using mso formulas over its bohm tree (as below).
And you were answering something about the higher order program being fully beta-reduced and encoded as a tree which apparently was supposed to turn it into a first order expression.
a program, on this setting, is something that returns a first order expression, i.e. it reads an input and returns an output being objects, not functions. however the program can still be higher order, calling functions and functions of functions, but at the end return an object. therefore it is of no surprise that the result of the execution (=beta reduction) doesn't end up with a function. however execution has a trace, and all possible traces (wrt all possible inputs) yields a tree, which is the bohm tree.
Then the tone quickly deteriorated, and you ended up rage quitting the conversation without finishing your explanation.
i really didnt see any point in explaining as every word i say is then (intentionally or not) misinterpreted to completely other fields. a good example is the mis-use of the term "higher order".
then i tried to see whether it's a misunderstanding problem or a personality problem, so i moved to speak about being gentleman.
As a result three questions / remarks which I found very interesting were left unanswered / undevelopped to my disappointment.
23:37 < HMC_a> so yes or no, is there a second(+) order expression which cannot be consistently proven in any mso framework? In general is full second/third order collapsible to msol, or isn't it?
that's just another mis-usage of the concept of order. as above. can you please explain me the question at the scope of verifying higher order programs? i dont see how the question make any sense. the program need not collapse to its spec (?!)
I expect this one must be discussed somewhere in the works of Bruno Courcelle so you could point us to some theorem or conjecture if that can save you some time with the explanations. Don't worry about making it understandable for the mere mortals. I'm happy with an explanation that I can't fully comprehend so long as HMC and you seem to be on the same page.
courcelle has nothing to do with program verification or stlc+y as far as i know.
he's the mso over graphs guy.
that all said, i'll really very happily explain anything, just please give me a question i can understand and not a paste of hmc's pile of buzzwords.
22:17 < HMC_a> but maybe I'm missing some collapsability magics, somewhere, so perhaps you could give a concrete example of verification of such an example?
I concur wholeheartedly with this one. A simple example of a second or third order program in STLC+Y with limited inputs, executed against all input combinations and encoded as a tree, and then the demonstration of how msol verifies it would be hugely helpful getting some intuitive understanding of how it works. That would give us the tools to try to find a case where it doesn't work (there shouldn't be any). You can recycle that explanation for the whitepaper, so no time wasted here.
here's a third order stlc program:
\x.\y.\z.x
the bohm tree looks like \x->\y->\z->"x"
i.e. is a list on this case (because we dont use application on this specific program).
now you can write an mso (or even fo) sentence "t is a leaf -> t's label is x" to verify that the program always returns x.
(this question was very specific so no problem answering it)
22:18 < naturalog> in bohm tree you dont have lambda terms
22:18 < naturalog> they're all reduced already
22:18 < naturalog> so the higher order rules disappear and remain only with true/false or other info
What kind of reduction are you talking about? How can the result not have lambda terms? Do you mean no lambda abstractions / bound variables? How do you guarantee that?
as explained above, a higher order program that returns an object is a first order term, no matter that inside it calls higher order terms. now, because it returns an object, it *must* beta-reduce to an object! after execution, you have no functions left, only data.
and again will gladly explain further.