> So I don’t agree that all proofs are useless. And also we see that a lot of > functional languages cleaned up their semantics precisely because they wanted > to prove things.
…absolutely. If theory is applied at the very beginning, it may prevent you from doing things that no one wants to prove later on. >>> On 27 Jan 2016, at 09:51, Pavel Velikhov <[email protected]> wrote: >>> >>> >>>> On 27 Jan 2016, at 12:37, Christian Grün <[email protected]> wrote: >>>> >>>>> Its a common practice for everybody, who needs to come up with formal >>>>> proofs. You start with the most simplified definitions possible, that >>>>> capture the essence of the problem. >>>>> Then you get the skeleton of the proof that is hopefully very simple. >>>>> Then you can add details back, hoping that the proof remains simple and >>>>> tractable. >>>>> >>>>> So imagine starting the proof while considering all the possible >>>>> variations of path expressions, all the Infoset stuff, all XML Schema >>>>> details. I think its hopeless. >>>> >>>> I’m completely in line with Michael’s observations. It would obviously >>>> be nice to have proofs for the full rule sets of the discussed >>>> languages; but as experience shows, no one will do it (the rare >>>> exception might prove the rule), so we are stuck with the work that is >>>> of limited practical use. >>> >>> I can’t agree with you. There are a lot of results that automatically hold >>> for the full specification, even though they are >>> proved on a clean and easy-to-use subset: undecidability and >>> np-completeness or np-hardness for instance. >>> >>> For the full specifications its sometimes hard to grasp the semantics, so >>> proving anything serious is impossible. >>> Example: try proving that SQL-2003 queries are equivalent to some superset >>> of relational algebra. >>> >> >> > _______________________________________________ [email protected] http://x-query.com/mailman/listinfo/talk
