Fak

Fak is an Esoteric programming language created by User:Yayimhere, which takes in set of axioms, an ordered list of functions, and an ordered list of atoms, and returns a (potentially) infinite set of atoms, and axioms for each one.

Syntax

The first section defines the set of functions. For example:

F .
FF .
. FFF .
...
FFF...FFF .
. FFF...FFFF .

note here the unary F thats used to order these functions, and they must be in order and start at F. here, FFF...FFF . is a unary function thats like, F(x), with application written as F x, and . FFF...FFF . is an infix operator, like x + y, ofc written x F y. These are all the functions. Then is the atom section, which is a single concatenation of the symbol H, on a single line. This defines the full set of atoms, which is all concatenations of H with length more than or equal to one, and less than or equal to the length of the given section. The last part program is made up of the axiom section listing each axiom:

L Axio1
LL Axio2
LLL Axio3
...
LLL...LLL AxioN

Each axiom must be an instance of "Rela" in the following BNF:

Var := Var Var | I
Expr := (Expr) | Expr Infx Expr | Unar Expr | Atom | Var
Equl := Expr == Expr | Expr =/= Expr | Expr :: Expr | Expr :/: Expr
Rela := (Rela) <> (Rela) | (Rela) > (Rela) | Equl

where Infx are the infix functions, Unar are the unary functions(both applied to an expr), and Atom is one of the atoms.

Semantics

First, it interprets the axiom section as, well, axioms, with == being equality, :: being exact syntactical identity(when looking at them, they are written the same, not caring about axiomatic equality), and the ones with crosses between them being a logical negation of those conditions, and <> being logical bidirectional implication, and > is single implication, and using the Var BNF as variables which could be any arbitrary expression(with brackets around it). all of these associate to the left(including the functions). Here, . First, it checks F H for equality to any of the atoms. If it is equal to any of the predefined atoms, it does nothing, moves on to the next item(using Prolog style theorem checking). Else, it assigns it the symbol L and prints L followed by a space and what it is equal to, and appends that to the list of atoms, as well as the axiom of what it is equal to(specifically L == ...), to the list of axioms. Then moves on to F HH and does the same, until all atoms have been checked, using L*y where y is the amount of L's in the last thing printed plus one, and * is the left character, appended to itself right side amount. Then it moves onto FF H, FF HH, and so on. Note that in the case of an infix, it treats H F y as the unary function, and after "completing" H F y, it does HH F y. Then, when every F and H has been done, it uses variables, incrementing within those until all have been used up again, nesting like this forever. So say we have F(infix), FF(unary), and H and HH, it would increment as:

H F H
H F HH
HH F H
HH F HH
FF H
FF HH
H F (H F H)
H F (H F HH)
H F (FF H)
H F (FF HH)
HH F (H F H)
HH F (H F HH)
...

Note that when the prover proves something about newly created atoms, it doesn't use their "atomic names" in the expression(though it does on the "other side" of the equality sign, so when testing if a generated expression is syntactically identical, it will do e :: L not whatever L represents). Also note that in expressions of the actual axiomatic system thats being used, brackets function as brackets. Note that it is assumed that for any expression X it is assumed it is equal to itself.

Examples

Looping Counter:

F .
H
L (I :/: II) <> (I =/= II)

this returns a symbol set which is infinite, and prints:

L F H
LL F F H
LLL F F F H
LLLL F F F F H
...

Empty set output:

F .
H
L F I == I