Posted: Mar 14, 2012 2:57 am
VazScep wrote:Yes, this is an excellent question. In fact, this is precisely the textbook definition of propositional logic, and was my first attempt at an implementation. It makes for a much simpler and elegant logical kernel. Specifically, you have made the axioms truly schematic. In my implementation, they are only "somewhat" schematic.
But consider proving a theorem such as, say, "P & Q -> Q & P" (see the Utils module to see how conjunction can be defined). Now, what would P and Q be? In most presentations of propositional logic, you start schematic and you stay schematic, so you'd have a function like:
- Code: Select all
conjComm p q :: Term a -> Term a -> Theorem a
This function would take two terms p and q and prove the theorem p & q -> q & p. To implement it, you'll eventually end up using the functions axiom1 and axiom2 and axiom3 and passing in various terms derived from p and q.
Just as the function axiom1 is a schematic axiom, the function conjComm is a schematic proof. It produces a different proof for every combination of p and q. Now suppose the proof is thousands of lines long (in this case, it isn't, but for theorems in industrial strength provers, you're frequently running to tens of millions). In that case, "Term 0 & Term 1 -> Term 1 & Term 0" requires running a few thousand lines of proof, while "Term 1 & Term 0 -> Term 0 & Term 1" requires running another few thousand lines of proof. That's bad news in terms of efficiency.
So the alternative is to fake the schema with a simple instantiation function. Now you can prove "Term 0 & Term 1 -> Term 1 & Term 0" and then use "inst ((-) 1)" to switch between the two without having to rerun the whole proof.
Yeah I see it now. I had been assuming that the only purpose of inst and friends was to instantiate the axioms, but now I see that you can use it to reinstantiate whole proofs. In this sense, there are really no non-schematic proofs, all proofs can be used as a schema to instantiate something else at least as complex as.
VazScep wrote:
I regard this as one of the differences between templates and type polymorphism. C++ templates are schematic in the first sense. ML-style polymorphism is "somewhat" schematic in the second sense. Neither is more expressive than the other (unless you start talking about loading new stuff at runtime without access to the compiler --- see my earlier example with Ocaml). But which one you want depends on how you're using them. The talk of explosions during template expansion is analogous to the explosion of proofs you'd get with your simpler logical kernel.
Yeah I see that now
VazScep wrote:
It is worth mentioning, I think, that Church's original paper on the Simple Theory of Types treated type variables schematically. It was Hindley and Milner who introduced ML-style polymorphism, which you add to simple type theory by providing a type instantiation rule. It doesn't buy you anything in terms of the expressive power of the logic, but it prevents explosions, and it's the route I followed in propositional logic.
Both ideas are brought together if you look at the inference rules of the theorem prover I use. There are two instantiation rules: one for variables, and one for types.
I see, I will take a look at that.
Any more interesting tidbits of related Haskell code?
VazScep wrote:Yeah, I can see the basic logic; I just can't identify with it. Both look like line noise to me.
You are saying that the important thing isn't the number of delimiters, but the variety of them. But in Haskell and ML, round brackets are basically the only delimiter. I see ML and Haskell structure mostly in the indentation, syntax highlighting, and blocking of code. You get all of that in Lisp too. At its worse, Lisp just has too many parentheses, which could be removed by imposing precedence rules, but I think that would make it harder for me to write macros.
Well, I meant the huge number of parentheses was only a facet of the problem.
If you say there is still one delimiter in Haskell, I agree, but the thing here is that it has a lot of other features that help you avoid running into a gazillion of them. Operator precedence like you said, the '$' and '.' operators go a long way helping here, 'if then else', 'do' and others also help.
VazScep wrote:Haha! I think we have a lot in common here. I better look into this ratpoison.
It is a lot simpler than any other window manager I ever saw. It basically is to X what gnu screen is to a terminal.
That it is simple goes a long way to explain why it is a pain in the ass to get it to work with newer applications, it implements almost no workarounds.
I also used wmii later, which works much better, and xmonad has always been in my 'to look at' list, but right now, with all the work and stuff, I need something which just works without much fiddling around, and that's why I have been using basically whatever the distro throws at me.
VazScep wrote:This one passed me by somehow. I'll check it out now.
Sure, but this one is quite longish