Examinable Invocation Vector

Examinable Invocation Vector (or EIV) is an untyped stateless functional programming language.
== Syntax ==
Syntax is similar to the lambda calculus notation, except that lambda symbols are omitted and arguments can be grouped. For example, lambda expression
 (λx.λy.yx)(λa.λb.λc.(ab)(ac))
can be writen in EIV as
 (x y.y x)(a b c.(a b)(a c))
Whitespace is necessary between identifiers, because identifiers may have multiple characters. Allowed characters in identifiers are all alphanumerics including hyphen and dash.
== I/O format ==
EIV doesn't have any constants or predefined functions. In order to explain how I/O operations work, we need to firstly define some functions. We say that
 0 = a b.b
 1 = a b.a
 P = a b c.c b a
 E = (f.f f)(f.P 0(f f))
Note: these functions are not predefined, we only introduce them in this text to explain I/O operations. Given input as a sequence of bytes, we convert it to bit array by concatenating reversed bits of each byte and we prepend 1 before each bit, then append infinitely many zeros. For example, input string abc will be converted to the following array of bits:
 111010101011111010111010101111101111101010111110000000000...
Then we construct a lambda expression from this array of bits. Suppose we have array of bits xyz000000..., we construct the lambda expression in the following manner (we named it S):
 S = P x(P y(P z E))
The result (named R) of the program execution is the lambda expression
 R = C S
where C is the program's source code. Then we reconstruct the output using the same I/O format. To be precise, we firstly check whether R 0 is 1, if it isn't then the output is empty. If it is, then the first output bit (the lowest bit of the first byte) is 1 iff R 1 0 is 1, otherwise it is 0. We do similarly for the rest of bits. Interpreter is not allowed to give wrong answer. If it can't prove or disprove that given expression is equal to 1, it must spin in an infinite loop, or report an error.
Input/output can also be a sequence of bits. Different implementations may define different I/O formats.
Also note that equality sign is not a part of the language, it is used here for readability.
== Examples ==
=== Cat ===
 a.a
Try it online
The cat program is identity function. When called with the input string, the program gives it back, and the output format is the same as input, therefore the string is the same.
=== Remove the first character ===
 (1 S.S 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1)(a b.a)
Try it online
This program simply skips the first 16 bits (one ASCII character, because of padding) and returns the remaining characters.
=== Replace the first character with a digit ===
 (0 1 P S.
 P 1(P 1(P 1 (P 1 (P 1(P 1(P 1 (P 0(
 P 1(P 1(P 1 (P 1 (P 1(P 0(P 1 (P 0(
 S 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
 ))))))))))))))))
 )(a b.b)(a b.a)(a b c.c b a)
Try it online
=== Reverse bits ===
 (0 1 P.
 (E.
 (f S.f f S E)(f s e.
 s 0(f f(s 1 1)(P 1(P(s 1 0)e)))e
 )
 )((f.f f)(f.P 0(f f)))
 )(a b.b)(a b.a)(a b c.c b a)
Try it online
=== Repeat the first character three times ===
 (input.
 (0 1 P.
 (E.
 (Byte.
 (first.
 (print.
 (f.f (f (f E)))(e.
 print e first
 )
 )(str b.
 (P 1 (P (b 0 0 0) (P 1 (P (b 0 0 1) (P 1 (P (b 0 1 0) (P 1 (P (b 0 1 1)
 (P 1 (P (b 1 0 0) (P 1 (P (b 1 0 1) (P 1 (P (b 1 1 0) (P 1 (P (b 1 1 1)
 str))))))))))))))))
 ))(
 Byte
 (input 1 0) (input 1 1 1 0) (input 1 1 1 1 1 0) (input 1 1 1 1 1 1 1 0)
 (input 1 1 1 1 1 1 1 1 1 0) (input 1 1 1 1 1 1 1 1 1 1 1 0)
 (input 1 1 1 1 1 1 1 1 1 1 1 1 1 0) (input 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0)
 ))(
 b0 b1 b2 b3 b4 b5 b6 b7 i j k.
 i(j(k b7 b6)(k b5 b4))(j(k b3 b2)(k b1 b0))
 ))((f.f f)(f.P 0(f f)))
 )(a b.b)(a b.a)(a b c.c b a))
Try it online
== Interpreters ==
* Interpreter
Category:Languages
Category:Functional paradigm
Category:Turing complete
Category:Implemented
Category:2019