reduce-equations

Simplify a set of equations by removing redundancies http://chriswarbo.net/projects/repos/reduce-equations.html

Latest on Hackage:0.1.1.0

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

BSD3 licensed by Chris Warburton
Maintained by chriswarbo@gmail.com
# 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](https://hackage.haskell.org/package/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](https://hackage.haskell.org/package/quickspec-0.9.6) library to do
the actual reduction. This relies heavily on existential types and Haskell's
[Typeable](https://hackage.haskell.org/package/base-4.9.0.0/docs/Data-Typeable.html)
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.
comments powered byDisqus