ZFC++

ZFC++ is a programming language which works with sets and performs operations on sets.
== Syntax ==
All values in this language are sets. A set can be empty, or can contain other sets. All sets are finite in size (but can be arbitrary large in size and depth).
Source code contains one or more function definitions. Each function takes zero or more arguments (sets) and returns a set as the result. Example of a function definition:
 func(x): x
It is a function named func that takes a set x as argument and returns the same set as the result.
Sets are represented using curly braces. For example:
 f(x, y): {x, y}
Function f here takes x and y as arguments and constructs (and returns) a set which contains x and y as elements.
== Operations on sets ==
There are only two operators on sets: ! and ~. Both operators are prefix unary operators.
The first operator ! takes a set as argument and if the set is non-empty returns the empty set, otherwise returns the singleton set whose only element is the empty set. For example, !{{}, {{}}} results in {} (because {{}, {{}}} is a non-empty set), while !{} results in {{}}.
The second operator ~ can be applied only in a function call and it calls the function with all elements of the given set and then computes the union of all returned values. For example:
 f(x, y): g(~x, y)
 g(x, y): {x, y}
Suppose that we call f with arguments {A, B, C} and D respectively (where A, B, C and D are some sets). So, we have f({A, B, C}, D). Now, it will be replaced with the expression from the definition of function f, which is g(~x, y). Formal argument x is substituted with {A, B, C} and y with D.
After substitution we have g(~{A, B, C}, D). Now, we apply the ~ operator. The result is the union of g(A, D), g(B, D) and g(C, D).
g(A, D) gives {A, D}
g(B, D) gives {B, D}
g(C, D) gives {C, D}
Taking the union of all those results, we obtain {A, B, C, D}, which is the result of f({A, B, C}, D) (note that it does not matter if some element is repeated multiple times - it is still the same set (duplicates are ignored)).
It is also possible to apply ~ to several arguments simultaneously. For example
 f(x, y): g(~x, ~~{x, y}, ~y)
 g(x, y, z): y
is also a valid program. We simply compute all results and take the union.
== Examples ==
Since there are literally no builtin functions, we need to construct everything from scratch.
First, we need some boolean types. Let the empty set represent a falsy value and any non-empty set represent a truthy value. We want to somehow be able to invert a boolean value. It is easy to implement a function for that:
 not(x): !x
It does exactly what we need. Now, we want to convert any non-empty set into {{}} and empty set into {}. It is also easy:
 bool(x): not(not(x))
To make code simpler, we explicitly define two values 0 and 1 in the following way:
 0: {}
 1: {0}
Note: they are just functions that take no arguments, so parentheses can be omitted.
Probably the most useful function is the union, so we can implement a function for that:
 union(x): union1(~x)
 union1(x): x
Explanation: function union returns the union of all elements of the given argument. It is done by using ~ operator. Function union1 is just a helper function.
Now, we want to somehow choose between two values depending on the truth value of some boolean. Here we have function if which takes three sets as arguments: x, y and z. If x is truthy (non-empty) then returns y, otherwise returns z:
 if(x, y, z): union({if1(~x, y), if1(~!x, z)})
 if1(x, y): y
Some simple logical operations:
 or(x, y): if(x, 1, y)
 and(x, y): if(x, y, 0)
 xor(x, y): if(x, !y, y)
If we have a set of boolean values and we want to know whether at least one is truthy (non-empty set) we can use function some, and if we want to know whether all of the elements are truthy we can use function every:
 some(x): union(x)
 every(x): not(some(every1(~x)))
 every1(x): {not(x)}
Then, we need a way to compare two arbitrary sets and determine whether they are equal or not. We also need a way to determine whether one set belongs to some other set. We can use previously defined functions to construct eq (returns a truthy value iff the two arguments are identical) and has (returns a truthy value iff the second argument belongs to the first argument):
 eq(x, y): if(x,
 if(y,
 and(
 every(eq1(x, ~y)),
 every(eq1(y, ~x))
 ), 0
 ), !y
 )
 eq1(x, y): {has(x, y)}
 
 has(x, y): some(has1(~x, y))
 has1(x, y): {eq(x, y)}
Explanation: it recursively compares each element of the first set with each element of the second set. Each element of the first set must be equal to at least one element of the second set and each element of the second set must be equal to at least one element of the first set. These two functions combined make indirect recursion.
Intersection and difference of two sets can be implemented in the following way:
 intersect(x, y): intersect1(x, ~y)
 intersect1(x, y): if(has(x, y), {y}, 0)
 
 diff(x, y): diff1(y, ~x)
 diff1(x, y): if(has(x, y), 0, {y})
We can also remove a single element y from the given set x:
 remove(x, y): diff(x, {y})
In order to introduce numbers, we can use Zermelo ordinals. For example, we can construct function size which returns the Zermelo ordinal representing the size of the given set:
 size(x): if(x, size1(x, ~x), 0)
 size1(x, y): {size(remove(x, y))}
Next, we can implement ordered pairs. We will use the short Kuratowski's definition for representing ordered pairs as sets. Namely, ordered pair (a, b) can be represented as {{a, b}, a}, so we can implement function pair to do exactly that:
 pair(x, y): {{x, y}, x}
And, of course, we can select the first element of a pair using function fst and we can select the second element using function snd:
 fst(x): fst1(~x, ~x)
 fst1(x, y): if(has(x, y), y, 0)
 
 snd(x): snd1(~x, ~x)
 snd1(x, y): if(has(x, y),
 if(eq(x, {y}),
 y,
 union(remove(x, y))
 ), 0
 )
We showed that all set operations can be implemented within the language. Proving Turing-completeness from here is simple.
== I/O format ==
Input is a set and output is also a set.
== Interpreters ==
Interpreter
Category:Languages
Category:Turing complete
Category:Implemented
Category:2020