Bidirectional proof refinement

16 March 2017 Rebecca Valentine 18 mins read

Bidirectional proof refinement - Input Output

In my last blog post, we looked at the very basics of proof refinement systems. I noted at the end that there was a big drawback of the systems as shown, namely that information flows only in one direction: from the root of a proof tree to the leaves. In this post, we'll see how to get information to flow in the opposite direction as well. The code for this blog post can be found on GitHub here.

Addition Again

The addition judgment Plus which we defined last time was a three-argument judgment. The judgment Plus L M N was a claim that N is the sum of L and M. But we might want to instead think about specifying only some of the arguments to this judgment. In a language like Prolog, this is implemented by the use of metavariables which get valued in the course of computation. In the proof refinement setting, however, we take a different approach. Instead, we make use of a notion called bidirectionality, where we specify that a judgment's arguments can come in two modes: input and output. This is somewhat related to viewing thing from a functional perspective, but in a more non-deterministic or relational fashion.

Let's start by deciding that the mode of the first two arguments to Plus is that of input, and the third is output. This way we'll think about actually computing the sum of two numbers. Instead of three Nat inputs, we'll instead use only two. We'll use a judgment name that reflects which two:

-- Haskell

data Judgment = Plus12 Nat Nat
  deriving (Show)
// JavaScript

function Plus12(x,y) {
    return { tag: "Plus12", args: [x,y] };
}

The behavior of the decomposer for Plus12 will have to be slightly different now, though, because there are only two arguments. But additionally, we want to not only expand a goal into subgoals, but also somehow synthesize a result from the results of the subgoals. So where before we had only to map from a goal to some new goals, now we must also provide something that maps from some subresults to a result.

Rather than giving two separate functions, we'll give a single function that returns both the new subgoals, and the function that composes a value from the values synthesized for those subgoals.

-- Haskell
decomposePlus12 :: Nat -> Nat -> Maybe ([Judgment], [Nat] -> Nat)
decomposePlus12 Zero y = Just ([], \zs -> y)
decomposePlus12 (Suc x) y = Just ([Plus12 x y], \[z] -> Suc z)

decompose :: Judgment -> Maybe ([Judgment], [Nat] -> Nat)
decompose (Plus12 x y) = decomposePlus12 x y
// JavaScript

function decomposePlus12(x,y) {
    if (x.tag === "Zero") {
        return Just([[], zs => y]);
    } else if (x.tag === "Suc") {
        return Just([[Plus12(x.arg,y)], zs => Suc(zs[0])]);
    }
}

function decompose(j) {
    if (j.tag === "Plus12") {
        return decomposePlus12(j.args[0], j.args[1]);
    }
}

The decompose function is somewhat redundant in this example, but the shape of the problem is preserved by having this redundancy. The same is true of the Maybe in the types. We can always decompose now, so the Nothing option is never used, but I'm keeping it here to maintain parallelism with the general framework.

Building a proof tree in this setting proceeds very similarly to how it did before, except now we need to make use of the synthesis functions in parallel with building a proof tree:

-- Haskell

findProof :: Judgment -> Maybe (ProofTree, Nat)
findProof j =
  case decompose j of
    Nothing -> Nothing
    Just (js, f) -> case sequence (map findProof js) of
      Nothing -> Nothing
      Just tns -> let (ts, ns) = unzip tns
                  in Just (ProofTree j ts, f ns)
// JavaScript

function unzip(xys) {
    var xs = [];
    var ys = [];

    for (var i = 0; i < xys.length; i++) {
        xs.push(xys[i][0]);
        ys.push(xys[i][1]);
    }

    return [xs,ys]
}

function findProof(j) {
    var mjs = decompose(j);

    if (mjs.tag === "Nothing") {
        return Nothing;
    } else if (mjs.tag === "Just") {
        var js = mjs.arg[0]
        var f = mjs.arg[1]
        var mtns = sequence(js.map(j => findProof(j)));

        if (mtns.tag === "Nothing") {
            return Nothing;
        } else if (mtns.tag === "Just") {
            var tsns = unzip(mtns.arg);
            return Just([ProofTree(j, tsns[0]), f(tsns[1])]);
        }
    }
}

Now when we run this on some inputs, we get back not only a proof tree, but also the resulting value, which is the Nat that would have been the third argument of Plus in the previous version of the system.

Let's now add another judgment, Plus13, which will synthesize the second argument of the original Plus judgment from the other two. Therefore, the judgment Plus13 L N means L subtracted from N. We'll add this judgment to the existing Judgment declarations.

-- Haskell

data Judgment = Plus12 Nat Nat | Plus13 Nat Nat
  deriving (Show)
// JavaScript

function Plus13(x,z) {
    return { tag: "Plus13", args: [x,z] };
}

We can now define a decomposition function for this judgment. Notice that this one is partial, in that, for some inputs, there's no decomposition because the first argument is larger than the second. We'll also extend the decompose function appropriately.

-- Haskell

decomposePlus13 :: Nat -> Nat -> Maybe ([Judgment], [Nat] -> Nat)
decomposePlus13 Zero z = Just ([], \xs -> z)
decomposePlus13 (Suc x) (Suc z) = Just ([Plus13 x z], \[x] -> x)
decomposePlus13 _ _ = Nothing

decompose :: Judgment -> Maybe ([Judgment], [Nat] -> Nat)
decompose (Plus12 x y) = decomposePlus12 x y
decompose (Plus13 x z) = decomposePlus13 x z
// JavaScript

function decomposePlus13(x,z) {
    if (x.tag === "Zero") {
        return Just([[], xs => z]);
    } else if (x.tag === "Suc" && z.tag === "Suc") {
        return Just([[Plus13(x.arg, z.arg)], xs => xs[0]]);
    } else {
        return Nothing;
    }
}

function decompose(j) {
    if (j.tag === "Plus12") {
        return decomposePlus12(j.args[0], j.args[1]);
    } else if (j.tag === "Plus13") {
        return decomposePlus13(j.args[0], j.args[1]);
    }
}

If we now try to find a proof for Plus13 (Suc Zero) (Suc (Suc (Suc Zero))), we get back Suc (Suc Zero), as expected, because 1 subtracted from 3 is 2. Similarly, if we try to find a proof for Plus13 (Suc (Suc Zero)) (Suc Zero), we find that we get no proof, because we can't subtract a number from something smaller than it.

Type Checking Again

We'll aim to do the same thing with the type checker as we did with addition. We'll split the HasType judgment into two judgments, Check and Synth. The Check judgment will be used precisely in those cases where a type must be provided for the proof to go through, while the Synth judgment will be used for cases where the structure of the program is enough to tell us its type.

-- Haskell

data Judgment = Check [(String,Type)] Program Type
              | Synth [(String,Type)] Program
  deriving (Show)
// JavaScript

function Check(g,m,a) {
    return { tag: "Check", args: [g,m,a] };
}

function Synth(g,m) {
    return { tag: "Synth", args: [g,m] };
}

Additionally, because of these changes in information flow, we'll remove some type annotations from the various program forms, and instead introduce a general type annotation form that will be used to shift between judgments explicitly.

-- Haskell

data Program = Var String | Ann Program Type
             | Pair Program Program | Fst Program | Snd Program
             | Lam String Program | App Program Program
  deriving (Show)
// JavaScript

function Var(x) {
    return { tag: "Var", arg: x };
}

function Ann(m,a) {
    return { tag: "Ann", args: [m,a] };
}

function Pair(m,n) {
    return { tag: "Pair", args: [m,n] };
}

function Fst(m) {
    return { tag: "Fst", arg: m };
}

function Snd(m) {
    return { tag: "Snd", arg: m };
}

function Lam(x,m) {
    return { tag: "Lam", args: [x,m] };
}

function App(m,n) {
    return { tag: "App", args: [m,n] };
}

The last change that we'll make will be to change the notion of synthesis a little bit from what we had before. In the addition section, we said merely that we needed a function that synthesized a new value from some subvalues. More generally, though, we need that process to be able to fail, because we wish to place constraints on the synthesized values. To capture this, we'll wrap the return type in Maybe.

-- Haskell

decomposeCheck
  :: [(String,Type)]
  -> Program
  -> Type
  -> Maybe ([Judgment], [Type] -> Maybe Type)
decomposeCheck g (Pair m n) (Prod a b) =
  Just ([Check g m a, Check g n b], \as -> Just undefined)
decomposeCheck g (Lam x m) (Arr a b) =
  Just ([Check ((x,a):g) m b], \as -> Just undefined)
decomposeCheck g m a =
  Just ( [Synth g m]
       , \[a2] -> if a == a2 then Just undefined else Nothing
       )

decomposeSynth
  :: [(String,Type)]
  -> Program
  -> Maybe ([Judgment], [Type] -> Maybe Type)
decomposeSynth g (Var x) =
  case lookup x g of
    Nothing -> Nothing
    Just a -> Just ([], \as -> Just a)
decomposeSynth g (Ann m a) =
  Just ([Check g m a], \as -> Just a)
decomposeSynth g (Fst p) =
  Just ( [Synth g p]
       , \[t] -> case t of
                   Prod a b -> Just a
                   _ -> Nothing
       )
decomposeSynth g (Snd p) =
  Just ( [Synth g p]
       , \[t] -> case t of
                   Prod a b -> Just b
                   _ -> Nothing
       )
decomposeSynth g (App f x) =
  Just ( [Synth g f, Synth g x]
       , \[s,t] -> case s of
                     Arr a b | a == t -> Just b
                     _ -> Nothing)
decomposeSynth _ _ = Nothing

decompose :: Judgment -> Maybe ([Judgment], [Type] -> Maybe Type)
decompose (Check g m a) = decomposeCheck g m a
decompose (Synth g m) = decomposeSynth g m
// JavaScript

function eq(x,y) {
  if (x instanceof Array && y instanceof Array) {
    if (x.length != y.length) { return false; }

    for (var i = 0; i < x.length; i++) {
      if (!eq(x[i], y[i])) { return false; }
    }

    return true;
  } else if (x.tag === y.tag) {
    if (x.args && y.args) {
      return eq(x.args,y.args);
    } else if (x.arg && y.arg) {
      return eq(x.arg,y.arg);
    } else if (!x.arg && !y.arg) {
      return true;
    } else {
      return false;
    }
  }
}

function decomposeCheck(g,m,a) {
    if (m.tag === "Pair" && a.tag === "Prod") {
        return Just([ [Check(g, m.args[0], a.args[0]),
                       Check(g, m.args[1], a.args[1])],
                      as => Just(undefined)]);
    } else if (m.tag === "Lam" && a.tag === "Arr") {
        return Just([ [Check([[m.args[0], a.args[0]]].concat(g),
                             m.args[1],
                             a.args[1])],
                      as => Just(undefined)]);
    } else {
        return Just([ [Synth(g,m,a)],
                      as => eq(a,as[0]) ? Just(undefined) : Nothing ])
    }
}

function decomposeSynth(g,m) {
    if (m.tag === "Var") {
        var ma = lookup(m.arg, g);

        if (ma.tag === "Nothing") {
            return Nothing;
        } else if (ma.tag === "Just") {
            return Just([[], as => Just(ma.arg)]);
        }
    } else if (m.tag === "Ann") {
        return Just([ [Check(g, m.args[0], m.args[1])],
                      as => Just(m.args[1]) ]);
    } else if (m.tag === "Fst") {
        return Just([ [Synth(g, m.arg)],
                      as => as[0].tag === "Prod" ?
                              Just(as[0].args[0]) :
                              Nothing ]);
    } else if (m.tag === "Snd") {
        return Just([ [Synth(g, m.arg)],
                      as => as[0].tag === "Prod" ?
                              Just(as[0].args[1]) :
                              Nothing ]);
    } else if (m.tag === "App") {
        return Just([ [Synth(g, m.args[0]), Synth(g, m.args[1])],
                      as => as[0].tag === "Arr" &&
                              eq(as[0].args[0], as[1]) ?
                                Just(as[0].args[1]) :
                                Nothing ]);
    } else {
        return Nothing;
    }
}

function decompose(j) {
    if (j.tag === "Check") {
        return decomposeCheck(j.args[0], j.args[1], j.args[2]);
    } else if (j.tag === "Synth") {
        return decomposeSynth(j.args[0], j.args[1]);
    }
}

Finally, the findProof function has to be augmented slightly to deal with the new Maybe in the return type of the synthesizing function:

-- Haskell

findProof :: Judgment -> Maybe (ProofTree, Type)
findProof j =
  case decompose j of
    Nothing -> Nothing
    Just (js,f) -> case sequence (map findProof js) of
      Nothing -> Nothing
      Just tsas ->
        let (ts,as) = unzip tsas
        in case f as of
             Nothing -> Nothing
             Just a -> Just (ProofTree j ts, a)
// JavaScript

function findProof(j) {
    var mjs = decompose(j);

    if (mjs.tag === "Nothing") {
        return Nothing;
    } else if (mjs.tag === "Just") {
        var js = mjs.arg[0]
        var f = mjs.arg[1]
        var mtns = sequence(js.map(j => findProof(j)));

        if (mtns.tag === "Nothing") {
            return Nothing;
        } else if (mtns.tag === "Just") {
            var tsns = unzip(mtns.arg);
            var mn = f(tsns[1]);

            if (mn.tag === "Nothing") {
                return Nothing;
            } else if (mn.tag === "Just") {
                return Just([ProofTree(j, tsns[0]), mn.arg]);
            }
        }
    }
}

If we now try to find proofs for some typical synthesis and checking examples, we find what we expect:

findProof (Check [] (Lam "p" (Fst (Var "p"))) (Arr (Prod Nat Nat) Nat))

findProof (Check [] (Lam "p" (Fst (Var "p"))) (Arr Nat Nat))

findProof (Synth [("p",Prod Nat Nat)] (Fst (Var "p")))

Conclusion

The bidirectional style in this post has some interesting limitations and drawbacks. Consider the case of the rule for App: it has to synthesize the type of both the function and the argument and then compare them appropriately. This means that certain programs require additional type annotations to be written. But this is somewhat unnecessary, because once we synthesize the type of the function, we can use that information to check the argument. In the next blog post, I'll try to explain how to do this in a more elegant way, the combines both the upward and downward flows of information.

If you have comments or questions, get in touch. I'm @psygnisfive on Twitter, augur on freenode (in #haskell).

This post is the second part of a three part series, the first part is here, and the third part is here.

Proof refinement basics

7 March 2017 Rebecca Valentine 19 mins read

Proof Refinement Basics - Input Output

Proof refinement basics

In this blog post, I'm going to discuss the overall structure of a proof refinement system. Such systems can be used for implementing automatic theorem provers, proof assistants, and type checkers for programming languages. The proof refinement literature is either old or hard to understand, so this post, and subsequent ones on the same topic, will present it in a more casual and current way. Work on proof refinement as a methodology for building type checkers and interactive proof systems has a long history, going back to LCF, HOL, Nuprl, and Coq. These techniques never really penetrated into the mainstream of programming language implementation, but perhaps this may change.

The GitHub repo for this project can be found here.

Prologue

As part of my work for IOHK, I've been designing and implementing a programming language called Plutus, which we use as the scripting language for our blockchains. Because IOHK cares deeply about the correctness of its systems, Plutus needs to be held to a very high standard, and needs to enable easy reasoning about its behavior. For that reason, I chose to make Plutus a pure, functional language with a static type system. Importantly, the language has a formal type theoretic specification.

To implement the type checker for the language, I used a fairly standard technique. However, recently I built a new framework for implementing programming languages which, while different from the usual way, has a more direct connection to the formal specification. This greater similarity makes it easier to check that the implementation is correct.

The framework also makes a number of bugs easier to eliminate. One class of bugs that arose a number of times in the first implementation was that of metavariables and unification. Because the language supports a certain about of unification-driven type inference, it's necessary to propagate updates to the information state of the type checking algorithm, so that everything is maximally informative and the algorithm can run correctly. Propagating this information by hand is error prone, and the new framework makes it possible to do it once and for all, in a bug-free way.

The framework additionally makes some features easier to program. For example, good error reporting is extremely important. But good error messages need to have certain information about where the error occurs. Not just where in the source code, but where in the logical structure of the program. All sorts of important information about the nature of the error, and the possible solutions, depend on that. The framework I developed also makes this incredibly easy to implement, so much so that it's build right into the system, and any language implemented using it can take advantage of it.

Proofs and Proof Systems

In the context of modern proof theory and type theory, a proof can be seen as a tree structure with labeled nodes and the class of proof trees which are valid is defined by a set of rules that specify how a node in a tree may relate to its child nodes. The labels, in the context of proofs, are usually hypothetical judgments, and the rules are inference rules, but you can also use the same conceptual framework for many other things.

An example of a rule is for any choice of A and B, if you can show that A is true and that B is true, then it's permissible to conclude A∧B is true. This is usually written with the notation

Maths

This rule explains one way that it's ok to have a node labeled A∧B is true in a proof tree, namely, when its child nodes are A is true and B is true. So this rule justifies the circled node in the following tree:

Maths

When used as a tool for constructing a proof, however, we think about rule use in a directional fashion. We start from the conclusion — the parent node — because this is what we'd like to show, and we work backwards to the premises of the rule — the child nodes — to justify the conclusion. We think of this as a dynamic process of building a proof tree, not simply having one. From that perspective, the rule says that to build a proof tree with the root labeled A&B is true, we can expand that node to have two child nodes A is true and B is true, and then try to build those trees.

In the dynamic setting, then, this rule means that we may turn the first tree below into the second:

Mathshttps://ucarecdn.com/651f5f86-0dde-4cdd-8c2f-850e62377635/)

 

Maths

In this setting, though, It's important to be aware of a distinction between two kinds of nodes: nodes which may appear in finished proof trees as is, and nodes which must still expanded before they can appear in a finished proof tree. In the above trees, we indicated this by the fact that the nodes which may appear in finished proof trees have a bar above them labeled by the name of the rule that justified them. Nodes which must still be expanded had no such bar, and we call them goals.

Building a Proof Refinement System

Let's now build a proof refinement system for a toy system, namely the system of equality (x == y) and addition (x + y = z) as relations among natural numbers. We'll implement it in both Haskell and JavaScript to give a sense of how things work. We'll start by just making the proof refiner system, with no interactivity nor any automatic driving of the proof system. We'll have to rely on the REPL to manage these things for us.

So the first thing we need is a definition of the naturals. In Haskell, we'll just use a normal algebraic data type, but in JavaScript, we'll use an object with a mandatory tag key and an optional arg key, together with helpers:

-- Haskell

data Nat = Zero | Suc Nat
  deriving (Show)
// JavaScript

var Zero = { tag: "Zero" };

function Suc(n) {
    return { tag: "Suc", arg: n };
}

Similarly, we'll define the judgments in question:

-- Haskell

data Judgment = Equal Nat Nat | Plus Nat Nat Nat
  deriving (Show)
// JavaScript

function Equal(x,y) {
    return { tag: "Equal", args: [x,y] };
}

function Plus(x,y,z) {
    return { tag: "Plus", args: [x,y,z] };
}

We'll next need some way to decompose a statement such as Plus (Suc Zero) (Suc Zero) Zero into subproblems that would justify it. We'll do this by defining a function that performs the decomposition, returning a list of new goals. But, because the decomposition might fail, we'll wrap this in a Maybe.

-- Haskell

decomposeEqual :: Nat -> Nat -> Maybe [Judgment]
decomposeEqual Zero Zero = Just []
decomposeEqual (Suc x) (Suc y) = Just [Equal x y]
decomposeEqual _ _ = Nothing

decomposePlus :: Nat -> Nat -> Nat -> Maybe [Judgment]
decomposePlus Zero y z = Just [Equal y z]
decomposePlus (Suc x) y (Suc z) = Just [Plus x y z]
decomposePlus _ _ _ = Nothing
// JavaScript

var Nothing = { tag: "Nothing" };

function Just(x) {
    return { tag: "Just", arg: x };
}

function decomposeEqual(x,y) {
    if (x.tag === "Zero" && y.tag == "Zero") {
        return Just([]);
    } else if (x.tag === "Suc" && y.tag === "Suc") {
        return Just([Equal(x.arg, y.arg)]);
    } else {
        return Nothing;
    }
}

function decomposePlus(x,y,z) {
    if (x.tag === "Zero") {
      return Just([Equal(y,z)]);  
    } else if (x.tag === "Suc" && z.tag === "Suc") {
        return Just([Plus(x.arg, y, z.arg)]);
    } else {
        return Nothing;
    }
}

If we explore what these mean when used, we can build some intuitions. If we want to decompose a judgment of the form Plus (Suc Zero) (Suc Zero) (Suc (Suc (Suc Zero))) in Haskell/Plus(Suc(Zero), Suc(Zero), Suc(Suc(Suc(Zero)))) in JavaScript, we simply apply the decomposePlus function to the three arguments of the judgment:

-- Haskell

decomposePlus (Suc Zero) (Suc Zero) (Suc (Suc (Suc Zero)))
  = Just [Plus Zero (Suc Zero) (Suc (Suc Zero))]
// JavaScript

decomposePlus(Suc(Zero), Suc(Zero), Suc(Suc(Suc(Zero))))
  = Just([Plus(Zero, Suc(Zero), Suc(Suc(Zero)))])

We'll define a general decompose function that will inspect a judgment and then call the appropriate decomposition function:

-- Haskell

decompose :: Judgment -> Maybe [Judgment]
decompose (Equal x y) = decomposeEqual x y
decompose (Plus x y z) = decomposePlus x y z
// JavaScript

function decompose(j) {
    if (j.tag === "Equal") {
        return decomposeEqual(j.args[0], j.args[1]);
    } else if (j.tag === "Plus") {
        return decomposePlus(j.args[0], j.args[1], j.args[2]);
    }
}

Now let's define what constitutes a proof tree:

-- Haskell

data ProofTree = ProofTree Judgment [ProofTree]
  deriving (Show)
// JavaScript

function ProofTree(c,ps) {
    return { tag: "ProofTree", args: [c,ps] };
}

The first argument of the constructor ProofTree is the label for the node, which is the conclusion of inference that justifies the node. The second argument is the sub-proofs that prove each of the premises of inference. So for example, the proof tree

Maths

would be represented by

-- Haskell

ProofTree (Plus (Suc (Suc Zero)) (Suc Zero) (Suc (Suc (Suc Zero))))
  [ ProofTree (Plus (Suc Zero) (Suc Zero) (Suc (Suc Zero)))
      [ ProofTree (Plus Zero (Suc Zero) (Suc Zero))
          [ ProofTree (Equal (Suc Zero) (Suc Zero))
              [ ProofTree (Equal Zero Zero)
                  []
              ]
          ]
      ]
  ]
// JavaScript

ProofTree(Plus(Suc(Suc(Zero)), Suc(Zero), Suc(Suc(Suc(Zero)))),
  [ ProofTree(Plus(Suc(Zero), Suc(Zero), Suc(Suc(Zero))),
      [ ProofTree(Plus(Zero, Suc(Zero), Suc(Zero)),
          [ ProofTree(Equal(Suc(Zero), Suc(Zero)),
              [ ProofTree(Equal(Zero,Zero)
                  [])
              ])
          ])
      ])
  ])

We now can build a function, findProof, which will use decompose to try to find a proof for any judgment that it's given:

-- Haskell

findProof :: Judgment -> Maybe ProofTree
findProof j =
  case decompose j of
    Nothing -> Nothing
    Just js -> case sequence (map findProof js) of
      Nothing -> Nothing
      Just ts -> Just (ProofTree j ts)
// JavaScript

function sequence(mxs) {
    var xs = [];

    for (var i = 0; i < mxs.length; i++) {
        if (mxs[i].tag === "Nothing") {
            return Nothing;
        } else if (mxs[i].tag === "Just") {
            xs.push(mxs[i].arg);
        }
    }

    return Just(xs);
}

function findProof(j) {
    var mjs = decompose(j);

    if (mjs.tag === "Nothing") {
        return Nothing;
    } else if (mjs.tag === "Just") {
        var mts = sequence(mjs.arg.map(j => findProof(j)));
        if (mts.tag === "Nothing") {
            return Nothing;
        } else if (mts.tag === "Just") {
            return Just(ProofTree(j, mts.arg));
        }
    }
}

If we now run this on some example triples of numbers, we find that it returns Justs of proof trees exactly when the statement is true, and the trees show just how the statement is true. Try it on the above example for suc(suc(zero)) + suc(zero) = suc(suc(suc(zero))).

The choice above to use the Maybe type operator reflects the idea that there is at most one proof of a judgment, but possible also none. If there can be many, then we need to use List instead, which would give us alternative definitions of the various functions:

-- Haskell

decomposeEqual :: Nat -> Nat -> [[Judgment]]
decomposeEqual Zero Zero = [[]]
decomposeEqual (Suc x) (Suc y) = [[Equal x y]]
decomposeEqual _ _ = []

decomposePlus :: Nat -> Nat -> Nat -> [[Judgment]]
decomposePlus Zero y z = [[Equal y z]]
decomposePlus (Suc x) y (Suc z) = [[Plus x y z]]
decomposePlus _ _ _ = []

decompose :: Judgment -> [[Judgment]]
decompose (Equal x y) = decomposeEqual x y
decompose (Plus x y z) = decomposePlus x y z

findProof :: Judgment -> [ProofTree]
findProof j =
  do js <- decompose j
     ts <- sequence (map findProof js)
     return (ProofTree j ts)
// JavaScript

function bind(xs,f) {
    if (xs.length === 0) {
        return [];
    } else {
        return f(xs[0]).concat(bind(xs.slice(1), f))
    }
}

function sequence(xss) {
    if (xss.length === 0) {
        return [[]];
    } else {
        return bind(xss[0], x =>
                 bind(sequence(xss.slice(1)), xs2 =>
                   [[x].concat(xs2)]));
    }
}

function findProof(j) {
    return bind(decompose(j), js =>
             bind(sequence(js.map(j2 => findProof(j2))), ts =>
               [ProofTree(j,ts)]));
}

In fact, Haskell lets us abstract over the choice of Maybe vs List, provided that the type operator is a monad.

A Type Checker with Proof Refinement

Let's now move on to building a type checker. We'll first define the types we're going to use. We'll have natural numbers, product types (pairs), and arrow types (functions). We'll also use a BNF definition as a reference:

<type> ::= "Nat" | <type> "×" <type> | <type> "→" <type>
-- Haskell

data Type = Nat | Prod Type Type | Arr Type Type
  deriving (Show)
// JavaScript

var Nat = { tag: "Nat" };

function Prod(a,b) {
    return { tag: "Prod", args: [a,b] };
}

function Arr(a,b) {
    return { tag: "Arr", args: [a,b] };
}

Next we must specify what qualifies as a program, which we'll be type checking:

<program> ::= <name> | "〈" <program> "," <program> "〉"
            | "fst" <program> | "snd" <program>
            | "λ" <name> "." <program> | <program> <program>
-- Haskell

data Program = Var String
             | Zero | Suc Program
             | Pair Program Program | Fst Type Program | Snd Type Program
             | Lam String Program | App Type Program Program
  deriving (Show)
// JavaScript

function Var(x) {
    return { tag: "Var", arg: x };
}

var Zero = { tag: "Zero" };

function Suc(m) {
    return { tag: "Suc", arg: m };
}

function Pair(m,n) {
    return { tag: "Pair", args: [m,n] };
}

function Fst(a,m) {
    return { tag: "Fst", args: [a,m] };
}

function Snd(a,m) {
    return { tag: "Snd", args: [a,m] };
}

function Lam(x,m) {
    return { tag: "Lam", args: [x,m] };
}

function App(a,m,n) {
    return { tag: "App", args: [a,m,n] };
}

The programs built with Fst, Snd, and App have more arguments that usual because we want to do only type checking, so we need to supply information that's not present in the types when working in a bottom up fashion. We'll see how we can avoid doing this later.

We'll also make use of a judgment HasType G M A, where G is a type context that assigns Types to variables (represented by a list of string-type pairs), M is some program, and A is some type.

-- Haskell

data Judgment = HasType [(String,Type)] Program Type
  deriving (Show)
// JavaScript

function HasType(g,m,a) {
    return { tag: "HasType", args: [g,m,a] };
}

We can now define the decompose functions for these. We'll just use the Maybe type for the decomposers here, because we don't need non-deterministic solutions. Type checkers either succeed or fail, and that's all.

-- Haskell

decomposeHasType
  :: [(String,Type)] -> Program -> Type -> Maybe [Judgment]
decomposeHasType g (Var x) a =
  case lookup x g of
    Nothing -> Nothing
    Just a2 -> if a == a2
               then Just []
               else Nothing
decomposeHasType g Zero Nat =
  Just []
decomposeHasType g (Suc m) Nat =
  Just [HasType g m Nat]
decomposeHasType g (Pair m n) (Prod a b) =
  Just [HasType g m a, HasType g n b]
decomposeHasType g (Fst b p) a =
  Just [HasType g p (Prod a b)]
decomposeHasType g (Snd a p) b =
  Just [HasType g p (Prod a b)]
decomposeHasType g (Lam x m) (Arr a b) =
  Just [HasType ((x,a):g) m b]
decomposeHasType g (App a m n) b =
  Just [HasType g m (Arr a b), HasType g n a]
decomposeHasType _ _ _ =
  Nothing

decompose :: Judgment -> Maybe [Judgment]
decompose (HasType g m a) = decomposeHasType g m a
// JavaScript

function lookup(x,xys) {
    for (var i = 0; i < xys.length; i++) {
        if (xys[i][0] === x) {
            return Just(xys[i][1]);
        }
    }

    return Nothing;
}

function decomposeHasType(g,m,a) {
    if (m.tag === "Var") {
        var ma2 = lookup(m.arg, g);

        if (ma2.tag === "Nothing") {
            return Nothing;
        } else if (ma2.tag === "Just") {
            return eq(a,ma2.arg) ? Just([]) : Nothing;
        }
    } else if (m.tag === "Zero" && a.tag === "Nat") {
      return Just([]);
    } else if (m.tag === "Suc" && a.tag === "Nat") {
      return Just([HasType(g, m.arg, Nat)]);
    } else if (m.tag === "Pair" && a.tag === "Prod") {
        return Just([HasType(g, m.args[0], a.args[0]),
                     HasType(g, m.args[1], a.args[1])])
    } else if (m.tag === "Fst") {
        return Just([HasType(g, m.args[1], Prod(a,m.args[0]))]);
    } else if (m.tag === "Snd") {
        return Just([HasType(g, m.args[1], Prod(m.args[0],a))]);
    } else if (m.tag === "Lam" && a.tag === "Arr") {
        return Just([HasType([[m.args[0],a.args[0]]].concat(g),
                             m.args[1],
                             a.args[1])]);
    } else if (m.tag === "App") {
        return Just([HasType(g, m.args[1], Arr(m.args[0],a)),
                     HasType(g, m.args[2], m.args[0])]);
    } else {
        return Nothing;
    }
}

function decompose(j) {
    if (j.tag === "HasType") {
        return decomposeHasType(j.args[0], j.args[1], j.args[2]);
    }
}

Using the same definitions of proof trees, sequencing, and finding a proof that we had earlier for Maybe, we can now perform some type checks on some programs. So for example, we can find that the program λx.x does indeed have the type Nat → Nat, or that it does not have the type (Nat × Nat) → Nat.

Conclusion

That about wraps it up for the basics of proof refinement. One thing to observe about the above system is that its unidirectional: information flows from the bottom to the top, justifying expansions of goals into subtrees. No information flows back down from subtrees to parent nodes. In my next blog post, I'll discuss how we might go about adding bidirectional information flow to such a system. This will allow us to perform type checking computations where a judgment might return some information to be used for determining if a node expansion is justified. The practical consequence is that our programs become less cluttered with extraneous information.

If you have comments or questions, get it touch. I'm @psygnisfive on Twitter, augur on freenode (in #languagengine and #haskell).

This post is the first part of a three part series, the second part is here, and the third part is here.

Thoughts on an ontology of smart contracts

6 March 2017 Charles Hoskinson 6 mins read

Thoughts on an ontology of smart contracts - Input Output

Thoughts on an ontology of smart contracts

The concept of smart contracts has grown considerably since the birth of Ethereum. We've seen an explosion of interdisciplinary research and experimentation bundling legal, social, economic, cryptographic and even philosophical concerns into a rather strange milieu of tokenized intellect. Yet despite this digital cambrian explosion of thought, there seems to be a lack of a unified ontology for smart contracts. What exactly is an ontology? Eschewing the philosophical sense of the word, an ontology is simply a framework for connecting concepts or groups alongside their properties to the relationships between them. It's a fundamental word that generally is the attempt at bedrock for a topic. For example, it's meaningful to discuss the ontology of democracy or the ontology of mathematics.

Why would one want to develop an ontology for smart contracts? What is gained from this exercise? Is it mostly an academic exercise or is there a prescriptive value to it? I suppose there are more questions to glean, but let's take a stab at the why.

Smart contracts are essentially two concepts mashed together. One is the notion of software. Cold, austere code that does as it is written and executes for the world to see. The other is the idea of an agreement between parties. Both have semantical demands that humans have traditionally had issues with and both have connections to worlds beyond the scope in which the contract lives.

Much of the focus of our current platforms, such as Ethereum, is on performance or security, yet abstracting to a more ontological viewpoint, one ought to ask about semantics and scope.

From a semantical perspective, we are trying to establish what the authors and users of smart contracts believe to be the purpose of the contract. Here we have consent, potential for non est factum style circumstances, a hierarchy of enforceability and other factors that have challenged contract law. What about cultural and linguistic barriers? Ambiguity is also king in this land.

Where normal contracts tend to pragmatically bind to a particular jurisdiction and set of interpretations with the escape hatch of arbitration or courts to parse purposeful ambiguity, decentralized machines have no such luxury. For better or worse, there is a pipeline with smart contracts that amplifies the semantical gap and then encapsulates the extracted consensus into code that again suffers from its own gap (Loi Luu demonstrated this recently using Oyente).

Then these structures presume dominion over something of value. Whether this dominion be data, tokens or markers that represent real life commitments or things such as deeds or titles. For the last category, like software giving recommendations to act on something in physical world, the program can tell one what to do, but someone has to do it.

So we have an object that combines software and agreements that has a deep semantic and scope concern, but one could add more dimensions. There is the question of establishing facts and events. The relationship with time. The levels of interpretation for any given agreement. Should everything be strictly speaking parsed by machines? Is there room for human judgement in this model (see Nick Szabo, Wet and dry code and this presentation)?

One could make a fair argument that one of the core pieces of complexity behind protocols like Ethereum is that it actually isn't just flirting with self-enforcing smart contracts. There are inherited notions from the Bitcoin ecosystem such as maximizing decentralization, maintaining a certain level of privacy, the use of a blockchain to order facts and events. Let's not even explore the native unit of account.

These concepts and utilities are fascinating, but contaminate attempts at a reasonable ontology that could be constructive. A less opinionated effort has come from the fintech world with both Christopher Clack's work on Smart Contract Templates and Willi Brammertz’s work on Project ACTUS. Here we don't need immutability or blockchains. The execution environment doesn't matter as much. It's more about consensus on intent and evaluation to optimize processes.

What about the relationship of smart contracts with other smart contracts? In the cryptocurrency space, we tend to be blockchain focused, yet this concept actually obfuscates that there are three data domains in a system that uses smart contracts.

The blockchain accounts for facts, events and value. There is a graph of smart contracts in relation to each other. Then there is a social graph of nodes or things that can interact with smart contracts. These are all incredibly different actors. Adding relays into the mix, one could even discuss the internet of smart contract systems.

Perhaps where an ontology could be most useful is on this last point. There seems to be economic value in marrying code to law for at least the purpose of standardization and efficiency, yet the hundreds of implicit assumptions and conditions upon which these systems are built need to be modelled explicitly for interoperability.

For example, if one takes a smart contract hosted on Rootstock and then via a relay communicates with a contract hosted on Ethereum and then connects to a data feed from a service such as Bloomberg offers, then what's the trust model? What assumptions has one made about the enforceability of this agreement, the actors who can influence it and the risk to the value contained? Like using dozens of software libraries with different licenses, one is creating a digital mess.

To wrap up some of my brief thoughts, I think we need to do the following. First, decouple smart contracts conceptually from blockchains and their associated principles. Second, come to grips with the semantic gap and also scope of enforcement. Third, model the relationships of smart contracts with each other, the actors who use them and related systems. Fourth, extract some patterns, standards and common use practices from already deployed contracts to see what we can infer. Finally, come up with better ways of making assumptions explicit.

The benefits of this approach seem to be making preparations for sorting out how one will design systems that host smart contracts and how such systems will relate to each other. There seems to be a profound lack of metadata for smart contracts floating around. Perhaps an ontology could provide a coherent way of labeling things?

Thanks for reading,

Charles

Centralized cryptocurrencies

5 March 2017 Alexander Chepurnoy 6 mins read

Centralized cryptocurrencies - Input Output

Centralized cryptocurrencies

This article is inspired by my recent visit to a blockchain technology conference and my discussions with colleagues about ideas to improve blockchain. Most of the conference speakers were from big Russian banks and their talks were about blockchain use cases, mainly as databases or smart contract platforms. However, none of the speakers were able to answer the question, ‘why did they really need blockchain?’. The correct answer for this question recently came from the R3 CEV consortium: "no blockchain because we don't need one". Blockchain is not needed for banks, it is needed instead of banks. It is required for decentralized systems only, applications with a trusted party will always be more efficient, simple, etc. The meaning of decentralization has been widely discussed (see, for example, this post from Vitalik Buterin and it is the only real purpose of blockchains. In this blog post I'm going to discuss the degree of centralization of existing cryptocurrencies and the reasons leading to it.

Governance and development centralization

Let's start with a non-technical topic. It is nice to think that no-one controls blockchain, ie that network participants (miners) act as a decentralized community and chose the direction of development. In fact, everything is much worse.

The first source of centralization here, is the source of the protocol for improvement. Only a small group of core developers is able to accept changes to the source code or even understand some protocol improvement proposals. No-one works for free and the organization that pays money to the core team in fact controls the cryptocurrency’s source code. For example, Bitcoin development is controlled by Blockstream, and this organization has its own interests. A treasury system like the one for Dash or the one proposed for Ethereum Classic may be the solution here. However, a lot of questions are still open (for example, the 78 pages of ETC treasury proposal are quite complicated, while the Dash treasury system was developed without any documentation).

The next centralization risk in governance is the cult of personality. While Vitalik tells us in his post, that no-one controls cryptocurrencies, his opinion is so important for the Ethereum community, that most of its members accepted the bailout of the DAO, which breaks the basic immutability principle of cryptocurrencies.

Finally, there are a lot of interested parties behind cryptocurrencies, and the opinion of some of them (for example the end users of the currency) is usually ignored. Anyway, the development of cryptocurrencies is a social consensus, and it is good to have a manifesto, declaring its purpose from the start.

Services centralization

One of the biggest problems with existing cryptocurrencies is the centralization of services. Blockchain processing is heavy (eg Ethereum processing from the genesis block may take weeks) and regular users that just want to send some coins have to trust centralized services. Most Bitcoin users trust blockchain.info, Ethereum users trust myetherwallet and so on. If these popular wallets were to be compromised, users’ funds would be lost.

Moreover, most users trust in blockchain explorers and never check that the blocks in it are correct. What is the meaning of the "decentralized" social network Steemit, if almost none of its users download a blockchain and believe that the data on Steemit.com is correct? Or imagine that blockchain.info was compromised: an attacker could steal all the users’ money from their wallets, hide the criminal transactions and show user-created transactions in blockchain explorer, and the attack could go unnoticed for a long time. Thus, trust in centralized services produces a single point of failure, allows censorship and puts user coins in jeopardy.

Mining centralization

With popular cryptocurrencies, hardware requirements are high even just for blockchain validation. Even if you own modern hardware able to process blocks fast, your network channel may not be wide enough to download the created blocks fast enough. This leads to a situation where only a few high-end computers are able to create new blocks, which leads to mining centralization. Being open by design, Bitcoin mining power is now concentrated in a limited group of miners, which could easily meet and agree to perform a 51% attack (or just censor selected transactions or blocks). Mining pools worsen the situation, for example, in Bitcoin just five mining pools control more than 50% of the hash rate (at least if you believe blockchain.info. Another option for miners is to skip transaction processing and produce empty blocks, which would also make blockchain meaningless.

Proof-of-Stake is usually regarded as more hardware friendly, however, a really popular blockchain requires a wide network channel to synchronize the network anyway. Also, it is usually unprofitable to keep a mining node in PoS and just a small percentage of coins are online that makes the network vulnerable. This is usually fixed by delegating mining power to someone else, that also leads to a small amount of mining nodes.

Centralization as a solution

The most scary point of all this is that more and more often, centralization is regarded as a solution for some problems of cryptocurrencies. To fix scalability issues, cryptocurrencies propose to use a limited number of trusted "masternodes", "witnesses", "delegates", "federations" and so on to "fix" the too-large amount of mining nodes in the network. The number of these trusted nodes may vary, but by using this method to fix scalability issues, developers also destroy the decentralized nature of the currency. Eventually this would lead to a cryptocurrency with only one performing node, that processes transactions very efficiently, without confirmation delays and forks, but suddenly a blockchain is not needed, as in R3's case.

Unfortunately, most users are not able to determine the lie in cryptocurrencies and like these centralized blockchains more and more, because for sure, the centralized way is (and will always be) more simple and user-friendly.

Conclusion

We are going to see more centralized cryptocurrencies and that will inevitably lead to mass disappointment in blockchain technology, because it is not needed for centralized solutions. It is still a user choice, whether to believe a beautiful and fast web interface or to use trustless, but harmful software, requiring you to download blockchain data and process it.

Most centralization risks may be fixed, if trustless full-nodes, wallets, explorers are cheap to launch and easy to use. I'm not going to propose a solution in this paper, but I hope it is coming soon!

Scotland and Japan launch IOHK's research network

28 February 2017 Jeremy Wood 4 mins read

Scotland and Japan launch IOHKs research network - Input Output

L-R: Nikos Bentenitis, IOHK Chief Operating Officer; Aggelos Kiayias, IOHK Chief Scientist; Charles Hoskinson, IOHK Chief Executive Officer and Co-Founder; Johanna Moore, Head of the School of Informatics, University of Edinburgh; Jon Oberlander, Assistant Principal for Data Technology, University of Edinburgh Research is at the core of what IOHK does so I am extremely proud of the company’s achievement in launching blockchain research centres at two world-class universities in February. This is a recognition of the pioneering work that IOHK is doing in advancing the science of cryptocurrencies, producing research that will all be open source and patent-free and progress the industry as a whole.

We marked the launch of our [Blockchain Technology Laboratory at the University of Edinburgh’s](http://www.ed.ac.uk/informatics/news-events/recentnews/beyond-bitcoiniohk-and-university-of-edinburgh "IOHK and University of Edinburgh Blockchain Technology Lab") School of Informatics last week, which will be led by Professor Aggelos Kiayias, our Chief Scientist. It is Scotland’s first blockchain research partnership between academia and industry, and we are proud to open it at the UK’s leading university for computer science research. Starting immediately, the lab will train the next generation of cryptographers and computer scientists, from undergraduate to post doctoral and professor level. The lab will be interdisciplinary, bringing in experts from the fields that blockchain encompasses, from law to ethics, and from economics to distributed systems. The research centre will also serve as the headquarters for IOHK’s growing network of global university partnerships.

The lab will provide a direct connection between developers and researchers, helping to get projects live faster and will pursue outreach projects with entrepreneurs in Edinburgh’s vibrant local technology community. Recruiting and outreach will begin immediately, and the full facility will be operational from summer 2017, located in the School of Informatics’ newly refurbished Appleton Tower.

Professor Kiayias says: “We are very excited regarding this collaboration on blockchain technology between the School of Informatics and IOHK. Distributed ledgers is an upcoming disruptive technology that can scale information services to a global level. The academic and industry connection forged by this collaboration puts the Blockchain Technology Lab at Edinburgh at the forefront of innovation in blockchain systems.”

And it was only two weeks earlier that IOHK celebrated another significant deal, at [Tokyo Institute of Technology](http://www.titech.ac.jp/english/news/2017/037573.html "IOHK and Tokyo Institute of Technology blockchain partnership"), a prestigious Japanese university and a leader in technology. Our partnership with them in setting up a Cryptocurrency Collaborative Research Chair is the first time the university has done such a deal and we are honoured to receive this distinction.

Two of our top researchers, Mario Larangeira and Bernado David will be embedded into a team led by Professor Tanaka at Tokyo Tech’s main site, the Ookayama campus. The team, along with professors and graduate students, will tackle industry challenges in this rapidly developing area of research into cryptocurrencies and provide education for the Japanese market. The partnership also includes support for students and researchers to attend international conferences.

Charles Hoskinson and Yoshinao Mishima,
President of Tokyo Tech

Tokyo Tech President, Yoshinao Mishima, says: “This agreement is important because Tokyo Tech is seeking to enhance the collaboration with industries and universities in Japan and abroad by producing groundbreaking results in research and engineering which will be published in internationally renowned scientific journals and conferences.”

These launches are just the beginning of a global network of research centres that IOHK is building, to drive collaboration between the world’s best cryptographers and developers to create the cutting edge blockchain technology that will revolutionise the world’s financial services. Further centres are planned in the US, Europe and beyond. Expect more news this year and in 2018.