rationalskepticism.org

mizvekov wrote:Cool. c++ has tuples now, with std::tuples. But they are "disconnected" from ordinary struct types which have basically the same form. boost Fusion is something that proposes to fix this, so you can declare an ordinary class and "map" it into an equivalent tuple, so you can mix the two forms freely.

Ah, that's interesting. I'm not sure whether it's a good idea to allow records and tuples to intermix like that. It breaks the abstraction. But then, it makes sense if you seriously want to regard records as just glorified tuples.

Personally, I like it. It's very much in the Haskell way of doing things, where a record with n fields is just sugar for a data constructor with n arguments.

VazScep wrote:Again, very cool. I suppose you have duck typing in C++ when you use template parameters. But there is no way to specify up front what characteristics a type must have to be acceptable, so it stays implicit in the code. When you pass the wrong type, the error happens inside the template definition, sometimes many layers deep, instead of at the point of instantiation.

It should be more powerful than C++ templates, much as simple polymorphism is (in some respects) more powerful than C++ templates. In particular, the binding is not resolved at compile-time. Thus, it is possible to load a native code library with a new set of class definitions at runtime, and have them work seamlessly with your existing duck-typed functions.

VazScep wrote:That's a capability missing from the c++ new standard. One of the reasons it's infamous for it's incomprehensible error messages is because, like I said, there is no way to specify restrictions on the types that can be passed as template parameters. So usually when you pass a nonsensical type, the error happens in implementation dependent code, sometimes many layers deep.

Is it also the case that templates can make inconsistent assumptions about each other? So you define a template which instantiates another in a way that is always going to lead to a type-error, and yet this is only known when you actually go ahead and instantiate that first template?

I'd say the difference between C++ templates and true polymorphism is that one is a schematic quantifier while the other is semantic quantifier. That's why, in C++, you can have an explosion in the number of classes and functions produced by templates, while things remain constant in Ocaml (at the expense of needing a hashtable to look up methods rather than a vtable).

I think there's a lot more to say about schematic versus semantic uses of quantifiers generally. God forbid it ever gets philosophical.

Yes. The new standard also defines a move semantics, and so you can declare a special kind of constructor, called a move constructor, which can "rob" another instance's internal data instead of copying it as in a copy constructor. That way it can make it pretty inexpensive to return complex data types, like std::vector, by value, where in the old standard there would be a superfluous copy of allocated data followed by the original being deleted.

Ah. Where would that be used? Presumably, you'd need guarantees that the original data wasn't being held by someone else?

VazScep wrote:Well capture by value/reference and mutable are orthogonal things. If you want the lambda to have it's own copy AND want to be able to modify it, then you would capture by value and declare the lambda as mutable. Likewise, if you want to see external modifications to that variable, AND also be able to modify that external variable, you would capture by reference and declare the lambda mutable.

I don't understand. Even if you don't declare the lambda mutable, what would happen if the lambda calls a destructive member function on the captured variable? Or is this more about assignment?

By the way, I have been playing with that example you sent me, but I am a bit confused about somethings.

Hey awesome! Glad you gave it a try!

Firstly, what are called "axioms" in the code are actually axiom schemes, right?

Yes. Though actually, in this code, everything is a scheme, axioms and theorems included.

In textbook presentations of this system, only axioms are schemes. However, you quickly realise as you go through the subsequent proof theory that everything is treated schematically: axioms, theorems and even the proofs. Technically, the proof that "P => P" is a completely different object to the proof that "Q => Q". But if you stick to this in an implementation, you're going to just see a huge explosion in the number of proof objects that you need to achieve anything (pretty much the exact situation you have with templates).

The alternative is to provide a new inference rule "inst" which allows you to instantiate any axiom and any theorem, by replacing variables systematically with arbitrary terms.

I have, however, made things perhaps a little bit too abstract. Normally, you think of variables in propositional logic as just strings, but they can be drawn from any set. And so, in this implementation, I've allowed variables to be drawn from any type. Simple string based variables are things like

Code: Select all

Var "p"

but you could just as easily have numerical variables as with

Code: Select all

Var 10

.

So for example, I can use that code to do things like this:

Code: Select all

*Propositional> let t1 = inst theoremTerm (Theorem (Var axiom1 :=>: Var axiom3))
*Propositional> let t2 = inst theoremTerm (Theorem (Var axiom1))

Ah, this is just a convenient trick of ghci. You've actually violated the encapsulation of the logical kernel. Save the code I provided you as a file "Propositional.hs". Then start a new file beginning with

Code: Select all

import Propositional

and load that. You'll now find that you cannot use "Theorem" as a data constructor.

The three axioms provided are schematic, and their variables are represented by strings. To instantiate the axioms, you supply a function which maps those strings to new terms. So you could, for instance, write

Code: Select all

> inst (\v -> if v == "p" then Var "q" else Var "r") axiom1
Theorem (Var "q" :=>: (Var "r" :=>: Var "q"))

For convenience, I have a set of utility functions here:

Code: Select all

module Utils where

import Propositional

import Data.List
import Data.Maybe (mapMaybe)

p = Var "p"
q = Var "q"
r = Var "r"

-- Derived syntax
p \/ q  = Not p :=>: q
p /\ q  = Not (p :=>: Not q)
p <=> q = (p :=>: q) /\ (q :=>: p)
t  = p :=>: p
f  = Not t
       
printTerm :: Term String -> String
printTerm (Var p)             = p
printTerm (Not (Var p))       = "~" ++ p
printTerm (Not (Not p))       = "~" ++ printTerm (Not p)
printTerm (Not p)             = "~(" ++ printTerm p ++ ")"
printTerm ((p :=>: q) :=>: r) = "(" ++ printTerm (p :=>: q) ++ ")"
                               ++ " ==> " ++ printTerm r
printTerm (p :=>: q)          = printTerm p ++ " ==> " ++ printTerm q

printThm thm = "|- " ++ printTerm (theoremTerm thm)

-- Retrieve the variable names in a term
vars :: Eq a => Term a -> [a]
vars (Var p)    = [p]
vars (Not p)    = vars p
vars (p :=>: q) = nub $ vars p ++ vars q
       
-- Instantiate variables in a term using a lookup
instTermM :: (Eq a) => (a -> Term b) -> [(a, Term b)] -> Term a -> Term b
instTermM dflt l = instTerm f
  where f p = maybe (dflt p) id (lookup p l)
       
-- Instantiate variables in a theorem using a lookup
instM :: (Eq a) => (a -> Term b) -> [(a, Term b)] -> Theorem a -> Theorem b
instM dflt l = inst f
  where f p = maybe (dflt p) id (lookup p l)
       
-- Instantiate variables in the order that they appear in a depth-first traversal
instL :: Eq a => [Term a] -> Theorem a -> Theorem a
instL l p = instM Var (zip (vars (theoremTerm p)) l) p
       
-- Append primes to ensure that the second argument does not appear in the first
avoid :: [String] -> String -> String
avoid ps p = p ++ replicate maxPrimes '\''
  where suffixes  = mapMaybe (stripPrefix p) ps
        maxPrimes = (maximum $ 0 : map primes suffixes)
        primes cs =
          case span (== '\'') cs of
            (ps,"") -> length ps + 1
            _       -> 0
           
-- Return an instantiation after matching two terms
match :: (Eq a, Eq b) => Term a -> Term b -> [[(a, Term b)]]
match = m []
  where m is (Var p) t =
          case lookup p is of
            Nothing -> [ (p, t) : is ]
            Just t' -> [ is | t == t' ]
        m is (Not t) (Not t')        = m is t t'
        m is (a :=>: c) (a' :=>: c') = concat [ m is' c c' | is' <- m is a a' ]
        m _ _ _                      = []


With these, you can now more simply write:

Code: Select all

> instL [q, p :=>: p] axiom1
Theorem (Var "q" :=>: ((Var "p" :=>: Var "p") :=>: Var "q"))

Which is alright and dandy, unless I am using that thing not the intended way, but I can't actually see how that can be used to represent a proof of a propositional logic theorem.

It's not obvious, don't worry. Here's a simple proof (actually the first proof from Mendelson's Mathematical Logic), showing that P => P:

Code: Select all

pp = do
  step1 <- mp (instL [p,p:=>:p,p] axiom2) (instL [p,p:=>:p] axiom1)
  return $ mp step1 (instL [p,p] axiom1)