## bin+lib relog

Strong String Normalization

### 14 stable releases

 1.0.13 Jan 6, 2024 Jan 3, 2024 Dec 25, 2023 Dec 5, 2023

#328 in Math

48KB
329 lines

# 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))}$$