### 14 stable releases

1.0.13 | Jan 6, 2024 |
---|---|

1.0.12 | Jan 3, 2024 |

1.0.11 | Dec 25, 2023 |

0.0.1 | Dec 5, 2023 |

#**328** in Math

**176** downloads per month

**MIT**license

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

with argument `a -> Maybe<a>`

`Int`

which would look like below:`a ``=` Int`;`
`Maybe``<`a`>`

when running this program the unification will bind

to `Int`

and return the result `a`

.`Maybe <Int>`

## Relog Type System

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