Utral

Utral is an esolang created by User:Yayimhere, to answer her very important question, "What if there was a negative null", and this answer's this question! It is based in Lambda Calculus, however that is only in underlying calculation, and not everything is a function, nor Is the main concept of Utral made specifically with Lambda Calculus in mind(however the creator has later used it minaly as lambda calculus).

Etymology

Utral's name comes from the idea of an un-neutral, as null is a sort of neutral value, it literally is nothing after all!

Info

the first, and most basic thing is the only real value/input in Utral, () which when passed to any function, will delete any mentions of the input name it was passed in by within the function, so passing () as an input to this function(note that this function wouldnt actually be written in utral):

λx.λy. x (y x)
would result in:
λy. y
which is the identity function. 

next is -z where z can be any Utral valid program, including the empty one. - applies the church integer negation function(However Utral doesnt have church integrals) to whatever z is. the function itself is:

(λz. (λa.λb.λf. f a b) ((λp. p (λa.λb. a)) z) ((λp. p (λa.λb. b)) z))

so we can derive -():

((λa.λb.λf. f a b) ((λp. p (λa.λb. a))) ((λp. p (λa.λb. b))))

now the last command is ., which is a postfix version of the Unlambda application operator(and technically there's also {} which is just brackets)

unlike some may assume, Utral will evaluate and simplify a specific function, just until it no longer can be evaluated nor simplified, and then that will be the final result.

some may also assume that Utral can use normal lambda calculus expression's outside of this syntax, however, that is also not true, as the above is the only valid syntax. As such, we derive this BNF for any program p in utral:

p = () | p p . | -p | { p }

Free variables

Some may want to use free variables in their expressions, and to that end, there's no set standard, however if you are implementing this, I recommend you allow them, since they are kinda useful. This ofc doesnt really change the power of Utral, as -x doesnt add a λx. to the expression, so it really doesnt change anything

Examples

Identity function or I:

{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . }

As we can simplify like this:

take the first innermost brackets:
     -() () . -> (λa.λb.λf. f a b) ((λp. p (λa.λb. a))) ((λp. p (λa.λb. b))) () . -> select the last expression when applicating: (λa.λb.λf. f a b) ((λp. p (λa.λb. a))) (((λa.λb. b)))
then do self application, as they are copied:
     (λa.λb.λf. f a b) ((λp. p (λa.λb. a))) (((λa.λb. b))) (λa.λb.λf. f a b) ((λp. p (λa.λb. a))) (((λa.λb. b))) -> (λb. (λa. (λb. b)))
then it is given to itself once: 
     (λb. (λa. (λb. b))) (λb. (λa. (λb. b))) -> (λa. (λb. b))
and then again:
     (λa. (λb. b)) (λb. (λa. (λb. b))) -> (λb. b)

As such, we have the identity function, though there propably is a better way to create it.

Reverse K or FALSE:

{ { { -{ { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } 
{ -() () . } . } . } } () . }
{ { { -() () . } { -() () . } . } 
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } . }

Since:

the first bracketed expression is a -I, so:
     -I -> λz. (λa.λb.λf. f a b) ((λp. p (λa.λb. a)) z) ((λp. p (λa.λb. b)) z) (λb. b) -> λz.z(λa.λb.a)(z(λa.λb.b)) -> λz.z(K(zK'))
then we pass it a ():
     λz.z(K(zK')) () . -> KK'
and then we pass the K an I, such that its selects the K':
     KK'I -> K'

As such, we have a K'.

A more "revolutionary" one, is K!:

{ { { { { -{ { { { -() () . } { -() () . } . } { { -() () . } 
{ -() () . } . } . } { { -() () . } { -() () . } . } . } } () . }  
{ { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . }
{ { -() () . } { -() () . } . } . } . } 
{ { { { -() () . } () . } () . } () . } . } () . }

Here's a pair constructor:

{ { { { { { -{ { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } } () . }  { { { -() () . }
{ -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . }

Here's a not:

{ { { { { { { { -{ { { { -() () . } { -() () . } . } { { -() () . }
{ -() () . } . } . } { { -() () . } { -() () . } . } . } } () . } 
{ { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . }
{ { -() () . } { -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . }
{ { { -{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . }
{ { -() () . } { -() () . } . } . } } () . }  { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } . } . }
{ { { { { -{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } } () . }  { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } . }

XOR:

{ { { { { { { -{ { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } } () . } 
{ { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . } 
{ { { { { { { { -{ { { { -() () . } { -() () . } . } { { -() () . }
{ -() () . } . } . } { { -() () . } { -() () . } . } . } } () . } 
{ { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . } { { { -{ { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } } () . }  { { { -() () . } { -() () . } . } { { -() () . }
{ -() () . } . } . } { { -() () . } { -() () . } . } . } . } . } { { { { { -{ { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } } () . }  { { { -() () . }
{ -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } . }
{ { { { -() () . } () . } () . } () . } . } () . } . } { { { { -() () . } { -() () . } . }
{ { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } }

XNOR:

{ { { { { { { { -{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } } () . } 
{ { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . } { { { { -() () . }
{ -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } . }
{ { { { { { { { -{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . }
{ { -() () . } { -() () . } . } . } } () . }  { { { -() () . } { -() () . } . } { { -() () . }
{ -() () . } . } . } { { -() () . } { -() () . } . } . } . } { { { { -() () . } () . } () . } () . } . } () . } -() . }
{ { { -{ { { { -() () . } { -() () . } . } { { -() () . } { -() () . } . } . }
{ { -() () . } { -() () . } . } . } } () . }  { { { -() () . }
{ -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . }
{ -() () . } . } . } . } . } { { { { { -{ { { { -() () . } { -() () . } . } { { -() () . }
{ -() () . } . } . } { { -() () . } { -() () . } . } . } } () . }  { { { -() () . }
{ -() () . } . } { { -() () . } { -() () . } . } . } { { -() () . } { -() () . } . } . } . }
{ { { { -() () . } () . } () . } () . } . } () . } . } . }