Reduce Equations

This package provides a command reduce-equations which reads in a list of equations from stdin, performs some simplification, and writes the results to stdout.

For example, given the equations a = b, b = c and a = c, one of these will be removed as it can be inferred from the other two. Similarly, given equations f a = g, f b = g and a = b, one of the first equations will be removed as it can be recovered by subtitution.

All of the real work is done by QuickSpec This package just provides stdio and machine-friendly formatting.

Formats

All IO is encoded in JSON. Both stdin and stdout should contain a single array of equations. The following example gives a single equation, which if written in a more human-friendly form, would be plus x x = times x 2:

[
 {"relation": "~=",
  "lhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int -> Int -> Int",
                                 "symbol": "plus"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role": "variable",
                        "type": "Int",
                        "id":   0}},
  "rhs":      {"role": "application",
               "lhs":  {"role": "application",
                        "lhs":  {"role":   "constant",
                                 "type":   "Int -> Int -> Int",
                                 "symbol": "times"},
                        "rhs":  {"role": "variable",
                                 "type": "Int",
                                 "id":   0}},
               "rhs":  {"role":   "constant",
                        "type":   "Int",
                        "symbol": "two"}}}
]

Equations

An equation is an object with the following values:

• relation: This is used mostly to identify that we've got an equation. In practice, this is always "~=" (what that means is up to you).
• lhs: this is a term, supposedly the left-hand-side of the equation, although the only difference from rhs is the name.
• rhs: this is a term, just like lhs except it's the right-hand-side.

Example:

{"relation": "~=",
  "lhs":     {"role": "application",
              "lhs":  {"role":   "constant",
                       "type":   "Bool -> Bool",
                       "symbol": "not"},
              "rhs":  {"role": "application",
                       "lhs": {"role":   "constant",
                               "type":   "Bool -> Bool",
                               "symbol": "not"},
                       "rhs": {"role": "variable",
                               "type": "Bool",
                               "id": 0}}},
  "rhs":     {"role": "variable",
              "type": "Bool",
              "id":   0}}

Terms

A term is an object containing a role, which is one of "constant", "variable" or "application". The other fields depend on what the term's role is:

• Constants
  • type: The type of the constant, a string written in Haskell's type notation. This is taken from the given function descriptions. For example "Int -> (Int -> Bool) -> IO Float"
  • symbol: The name of the constant, as a string. For example "reverse".
• Variables
  • type: The type of the variable, a string written in Haskell's type notation. The types can be made up, but they should be consistent (e.g. both sides of an equation should have the same type; application should be well-typed; etc.). Unification of polymorphic types isn't supported; types are identified syntactically. For example "[Int]".
  • "id": A numeric ID for the variable. IDs start at 0. Used to distinguish between multiple variables of the same type. Variable ID only matters within a single equation. For example, to represent three integer variables we might use {"role": "variable", "type": "Int", "id":0}, {"role": "variable", "type": "Int", "id":1} and {"role": "variable", "type": "Int", "id":2}.
• Applications
  • lhs: A term representing a function to apply.
  • rhs: A term representing the argument to apply the lhs function to. Functions are curried, so calling with multiple arguments should be done via a left-leaning tree.

Implementation Notes

We co-opt the equation-reducing machinery of the QuickSpec library to do the actual reduction. This relies heavily on existential types and Haskell's Typeable mechanism.

Since the incoming equations may have arbitrary types, and GHC doesn't let us define custom Typeable instances, we perform a conversion step:

• Once an array of equations has been parsed, we recurse through the terms and switch out each distinct type with a freshly-generated replacement, of the form Z, S Z, S (S Z), etc. (these are just Peano numerals, e.g. see https://en.wikipedia.org/wiki/Successor_function )
• We provide special functions getRep and getVal to plumb these Peano types into QuickSpec's machinery, convincing it that we have a signature of well-typed terms.
• We reduce the given equations, with their switched-out types, to get a reduced set.
• We switch back the types for presentation purposes, pretty-printing to JSON.