Thoughts on Rejoice

On Linear Logic

Traditional logic treats propositions as inexhaustible, whereas linear logic accounts for resources, using something changes the world. This is illustrated with file handles: once the file is consumed, any fraction requiring it in its denominator simply won't fire; the resource is inaccessible through absence rather than enforcement.

file^1
	closed/file
	read/file ( unreachable )

A one-shot fraction can freely duplicate or discard symbols(x^2/x), but the fraction itself is consumed after firing. Anonymous functions and the @label mechanism are what promote rules to unlimited use.

coin^3

@VendingMachine ( coin -- candy )
	[VendingMachine candy]/coin

Typically, resource tracking constrains what programmers can do with values, but here, entities persist because nothing consumed them, not because they're protected.

On Reversibility

Multiplying by the inverse of a fraction undoes the application of that fraction, allowing for a certain level of reversibility at the operand level. A program is reversible if it has exactly one forward rule match per input state and exactly one reverse rule match per output state. If that holds, the system cannot lose information.

a^3 b^2 ( fwd ) '[a c]/b -> a^5 c^2
a^5 c^2	( bwd ) 'b/[a c] -> a^3 b^2

To find if a program is within the subset of reversible programs: ignore any program with labels and check if there are any pairs of fractions whose denominators are compatible with the same input bag but whose numerators produce the same output. For example, the OR gate is provably irreversible at compile-time, due to having converging outputs on true.

x y or
    true/[x y or]
    true/[x or]
    true/[y or]
    false/or

On Optimization

There are various levels of optimizations possible, the interpreter might choose to drain symbols by anonymous functions in a single step. This allows for moving or copying values from a single denominator to any number of symbols, without having to run through each value one at a time. But each layer of optimization adds runtime costs.

• 'x/a: One symbol to another.
• '[x y]/a: One symbol to many symbols.
• '[x^2 y]/a: One symbol to many symbols, multiple values at a time.
• '[x^2 y]/a^4: Multiple values from one symbol to many symbols.
• '[x^2 y]/[a^4 b^3]: Multiple values from multiple symbols to many symbols.

c^5 '[a b]/c ( c = 5; a = b = c; )

[c^5] '[a b]/c 
[c^4 a b] '[a b]/c 
[c^3 a^2 b^2] '[a b]/c 
[c^2 a^3 b^3] '[a b]/c 
[c a^4 b^4] '[a b]/c 
[a^5 b^5] '[a b]/c 
[a^5 b^5] 

Many of these loop-shaped behaviors are better handled explicitly with variable exponents instead of labels:

c^5 [a^c b^c]/c^c ( c = 5; a = b = c; )

[c^5] [a^c b^c]/c^c 
[a^5 b^5] 

On Fractran

A Fractran program can be thought of as a Rejoice program with a single label, at the top of the program, present in each numerator. For example, the Fractran program: [3^2 5^2], 7/3, 7/5

r3^2 r5^2

@Fractran ( r3 r5 -- r3+r5.r7 )
	[Fractran r7]/r3
	[Fractran r7]/r5

[r3^2 r5^2] [Fractran r7]/r3 [Fractran r7]/r5 
[r3 r5^2 r7] [Fractran r7]/r3 [Fractran r7]/r5 
[r5^2 r7^2] [Fractran r7]/r3 [Fractran r7]/r5 
[r5^2 r7^2] [Fractran r7]/r5 
[r5 r7^3] [Fractran r7]/r3 [Fractran r7]/r5 
[r5 r7^3] [Fractran r7]/r5 
[r7^4] [Fractran r7]/r3 [Fractran r7]/r5 
[r7^4] [Fractran r7]/r5 
[r7^4]

Fractran programs seem to be a subset of Rejoice programs, a fraction with variable exponents alone would need one Fractran fraction per possible exponent value, and since the exponents are unbounded, there would need an infinite amount of fractran fractions to emulate it. That difference makes Rejoice a higher-order multiset system.

Bestiary