Relog

An implementation of several strongly-normalizing string rewriting systems

Relog (Reduction Logic) Flavor

a = Int;
List<a>
---output----
List<Int>

A<b,C<d>> = A<Int,C<Bool>>;
R<b>
---output-------------------
R<Int>

A<b,c> := R<c>;
A<B,C>
---output----------
R<C>

Print<"hello world">
---output-----------
[stdout]hello world
0

For<n,99,0,
   Print<"{n} bottles of beer on the wall
        \r{n} bottles of beer
        \rTake one down, pass it around
        \r{n} bottles of beer on the wall">
>
---output------------------------------
[stdout]99 bottles of beer on the wall
...
0

Relog Syntax

Relog is a type system, not a programming language. It is not Turing Complete, it is Strongly Normalizing.

The basic syntax of a Relog program is defined by unifications, followed by a result.

Unifications have a left-hand-side and a right-hand-side separated by an equal sign with a semicolon after each unification:

Pair<a,b> = Pair<Int,Int>;

Results are a single term and can reference unification variables bound by previous actions:

Pair<a,a>

An example program might represent the application of a function a -> Maybe<a> with argument Int which would look like below:

a = Int;
Maybe<a>

when running this program the unification will bind Int to a and return the result Maybe<Int>.

Relog Type System

$$apply \ \ \frac{unify(f,fx)⊢r}{f⇻r⊢reify(apply(r))}$$