rationalskepticism.org

mizvekov wrote:Okay, I am a bit stumped on this one.

I'd expect you to be. I've thrown you in at the deep end wearing concrete shoes.

I think that I need axiom3 to prove it, and this axiom cannot be used implicitly from this proof language, so I need to instantiate it manually and then bring it into the proof by using the UseTheorem constructor.

Right. Actually, I've used the axiom twice with two different instantiations. Rather than doing the instantiation manually, you might find this function helps:

Code: Select all

-- matchMP ( Γ ⊢ (P → Q) (Δ ⊢ P') attempts to match P with P', and then applies MP.
matchMP :: Theorem String -> Proof -> Proof
matchMP imp ant =
  let antT = concl ant in
    case theoremTerm imp of
      p :=>: q ->
        case match p antT of
          [insts] -> MP (UseTheorem $ instM Var insts imp) ant
          _       -> error "MATCH MP"
      _ -> error "MATCH MP"

This function is like mp, but it will try to instantiate the second argument to make it line up with the first.

The reason I need it is because I need the following auxiliary theorems:
1) |- (~p -> ~q) -> (q -> p)
2) |- (~p -> q) -> (~q -> p)

Number 1 is easy to do with "instL [p, q] axiom3".
Now number 2 is hard. Maybe it's just my mind being burned out from making sense of all that code and then trying to solve this, but anyway, if I do "instL [p, Not q] axiom3" then I get "|- (~p ==> ~~q) ==> ~q ==> p", and so I still have that double negation, which I have to get rid of. So I would need a theorem like: "|- (p ==> q) ==> (p ==> ~~q)", and this last one I am not seeing how to prove...
Will give it another go tomorrow.

It might be that you are trying to prove something that is more aptly derived from the exercise theorem. Note though, that it took me 16 proof steps in all to do this.

VazScep wrote:Okay, but still I need to be able to prove that one with just these 3 axioms!

Yeah, there's a fair bit of work to go. My Bootstrap file is 425 lines of proof.

VazScep wrote:Yes, and I also remember that monads are another example of a combinator language, so I know I have used them, but I never tried implementing a new one yet.

Yes. In fact, I'd say that the monad combinators are an abstraction over various other combinator languages.

VazScep wrote:That irks me a bit. Perhaps I am being too naive here, but I think the universities place is to teach students how to think and learn for themselves, and not to focus too much on directly teaching trade skills.

Not sure. I'd struggle to be able to give a definition of computer science and what a computer science degree should entail. At one end, if it's just the professional degree of a programmer, then I guess they should be expected to learn as many trade skills as a mechanical engineer

VazScep wrote:I am not so sure here. I understand that haskell makes it a lot easier for someone who is trying to make a program and prove that it is bug free, but I am not so sure if it would significantly reduce the number of bugs when it's the joe average industry programmer. There is just a lot of bugs that the type system will not catch.

Heretic! If it types, it's correct!

Yeah, maybe there's more to this, or maybe less. I'm just trying to think of reasons why Common Lisp was made to be so dynamic.

VazScep wrote:I see. But then are these interpreter sessions secure? I mean I get the impression that whoever is using it could just do something similar to what I did and violate the encapsulation of the kernel.

Well, you can't pull that trick off in Ocaml. But you could always violate the encapsulation just by changing the kernel code.

The type of security here is more like self-assurance. I want to trust that I haven't violated encapsulation, and that the tools I write aren't cheating. If any tool, no matter how complex and opaque, manages to produce an object that types as a theorem, I have an extremely strong guarantee from the type system that it went through the kernel.

The sort of security I don't have is security from a malicious programmer, who perhaps used "Obj.magic" to circumvent the type system, or exploited a vulnerability in the Ocaml interpreter, or customised the pretty printer to render his trivial theorem that "1 + 1 = 2" as the statement of Fermat's Last Theorem.

I can imagine a world where we actually start paying people large sums of money to do significant formalisation work. We'll probably have to be more concerned then with cheaters.