User:Junkshipp/Sandbox

Duchathair is a functional programming language inspired by PRA and theorem provers. Duchathair can be used to define functions and prove theorems about them. The language is esoteric due to its minimalism, which can make even simple statements hard to prove.

Basic syntax

Whitespace and comments

The meaningful characters are the following:

• The 52 uppercase and lowercase letters of English
• The symbols 0, ;, +, _, ", and #

Characters not on this list are all treated as the same "space" character. Adjacent instances of "space" characters are treated as a single instance.

Anything written between "" is ignored, and the whole substring, including the quotes, is treated as a "space" character. This facilitates comments.

Commands

Commands typically consist of a name, a keyword (always begins with #), and one or more expressions, functions, or results, depending on the keyword. Each command before the last one must be is terminated by a semicolon. Such a command is essentially a definition for the name, assigning a function or a result to it, based on the keyword. It is also possible to write a command consisting solely of the name of a result (note: the equality it represents is printed). An empty command is also valid, though does nothing.

Functions

Calling functions

Duchathair essentially uses Polish notation for calling functions, eliminating the need for brackets. So, instead of something like a * b, the notation used is times a b. Additionally, there's a single unary operation, +, which denotes the successor of a number. The space between + and its operand is optional. Additionally, 0, x, and y are available and 0-ary.

Defining functions

There are a two keywords that can be used to define functions: #fn and #pr. All user defined functions are binary (i.e. they take two arguments).

The syntax for defining a new function with #fn is the following:

example #fn times x times y x;

This line defines a function example that, when called with two arguments x and y, returns x*(y*x), assuming times is defined by the user as usual.

Functions can also be defined with #pr, which stands for primitive recursive.

prtest #pr +y add y prtest x y;

This line defines a function that returns +y when called with 0 and y and add y prtest x y when called with +x and y. So, defining a function with #pr requires two expressions, one for when the first argument is 0 and the other for when it is larger. The first expression may only use y, not x. The second expression can use both and additionally function x y, where function represents the function being defined and the arguments are exactly x and y.

Outside of that, one can only use previously defined functions in definitions. One cannot define a function with the same name as a previously defined function or result. Function names may only use the English letters and underscore. Sole x and y are reserved and cannot be used for names.

Note the semicolon at the end. Each function definition must end with one, unless the command in question is the last one.

Deduction

Results are proven facts about functions. Each result represents an equation between two expressions. Such equalities are derived from other results and functions using keywords like #pl. Here are examples of each keyword used for deduction. Note that a command with just the name of a result causes the equality it stands for to be printed.

#pl - Plugging in expressions

f #fn add x times x y; "Defining a function f"
Basic_f_equality #pl f x y;
Basic_f_equality; "Output: f x y = add x times x y"
Another_f_equality #pl f 0 +0;
Another_f_equality; "Output: f 0 +0 = add 0 times 0 +0"

The keyword #pl takes a function and two expressions, creating an equality between with LHS as the function and the arguments and the RHS with the arguments in the place of x and y in the definition. No other simplification is done.

The previous example dealt with functions defined using #fn. When #pl is used with functions defined using #pr, the first argument must be either 0 (verbatim; not just equal to 0) or preceded by a + (the successor operation). This allows #pl to decide which part of the definition of a #pr function to use.

g #pr ++y times x g x y; "Defining a function g"
Case_first_argument_zero #pl g 0 y;
Case_first_argument_zero; "Output: g 0 y = ++y"
Otherwise #pl g +x y;
Otherwise; "Output: g +x y = times x g x y"

#id - More plugging in

The principle that #id is based on is that if LHS and RHS are equal, applying a function to both sides keeps the equality. Since all user-defined functions are binary, #id has the user give one function and two proven equalities (results, by name).

"Assume these two equalities have already been proven 
and the functions in question defined."
Arbitrary_identity; "Output: h x 0 = i 0 x"
Another_identity; "Output: i x x = h 0 x"
Result #id j Arbitrary_identity Another_identity;
Result; "Output: j h x 0 i x x = j i 0 x h 0 x"

#eq - Equality

"Assume these two equalities have already been proven
and the functions in question defined."
First_equality; "Output: k x y = l x +y"
Second_equality; "Output: k x y = m y x"
Third_equality #eq First_equality Second_equality;
Third_equality; "Output: l x +y = m y x"

Essentially, #eq derives B = C from A = B and A = C, where A, B, and C represent arbitrary expressions. This can be used with other keywords to derive various things, such as commutativity and transitivity for all expressions.

#in - Induction

"Assume stuff has been already defined and proved."
Base; "Output: foo 0 y = bar 0 y"
Step_first; "Output: foo +x y = qux x foo x y"
Step_second; "Output: bar +x y = qux x bar x y"
Induction #in Base Step_first Step_second;
Induction; "Output: foo x y = bar x y"

Induction is implemented using #in, which takes three results, deducing that two functions are the same for all x and y. The first argument is a base case stating that two functions are the same when the first term is 0. The second and third argument show for both functions that when +x is passed as the first argument and y as the second, this is equal to when x and the value of the function at x and y are passed as arguments to some third function, same in both cases.

Notes

One can only use previously defined results in deduction. One cannot define a result with the same name as a previously defined function or result. Result names may only use the English letters and underscore. Sole x and y are reserved and cannot be used for names.

Example code

The following code defines add and proves it commutes. Not yet, though, as it's unfinished.

add #pr y +add x y; "Definition of add"

adds #fn add x +y;
ADDS_L #pl adds 0 y;
ADDS_LL #pl add 0 +y;
adds_u #fn adds 0 y;
ADDS_U_L #pl adds_u x y;
ADDS_LLL #eq ADDS_U_L ADDS_U_L;
ADDS_LLLL #eq ADDS_LLL ADDS_L;
ADDS_LLLLL #eq ADDS_LL ADDS_LLLL;
sl #fn +y;
sadd #fn +add x y;
SADD_L #pl sadd 0 y;
SADD_LL #pl add 0 y;
SADD_LLL #id sl SADD_LL SADD_LL;
SL_L #pl sl add 0 y add 0 y; 
SADD_LLLL #eq SADD_LLL SL_L;
SL_LL #pl sl y y;
SADD_LLLLL #eq SADD_LLLL SL_LL;
sadd_u #fn sadd 0 y;
SADD_U_L #pl sadd u x y;
SADD_LLLLLL #eq SADD_U_L SADD_U_L;
SADD_LLLLLLL #eq SADD_L SADD_LLLLLL;
SADD_LLLLLLLL #eq SADD_LLLLL SADD_LLLLLLL;
ADDS_SADD #eq ADDS_LLLLL SADD_LLLLLLLL; "adds 0 y = sadd 0 y"

ADDS_ST_L #pl adds +x y; "adds +x y = add +x +y"
adds_st_u #fn adds +x y;
ADDS_ST_U_L #pl adds_st_u x y;
ADDS_ST_LL #eq ADDS_ST_U_L ADDS_ST_U_L;
ADDS_ST_LLL ADDS_ST_L ADDS_ST_LL;
ADDS_ST_LLLL #pl add +x +y; "add +x +y = +add x +y"
ADDS_ST_SL_L #pl sl x adds x y;
ADDS_ST_SL_L 

WIP, unfinished. the following is informal drafting

subgoal:
add x +y = + add x y
that is adds x y = sadd x y
proof. [adds 0 y = sadd 0 y] (gotten) [adds +x y = sl x adds x y] (ez) [sadd +x y = sl x sadd x y] (ez)

subgoal: 
radd +x y = + radd x y

WIP, unfinished. the following is informal drafting
near #in [add 0 y = radd 0 y](ez) [add +x y = sucoflast x add x y](ez) [radd +x y = sucoflast x radd x y] (hard?)

The same deal, but with tabulation, comments, and extra characters. Due to the way whitespace works, the following piece of code is equally valid Duchathair.

"PROVING THE COMMUTATIVITY OF ADDITION"

"Definition." add #pr {
   "add(0,  y)" = y,
   "add(+x, y)" = +add(x, y);
}

"To prove add commutes, we need to show add(x, y) = add(y, x)."

WIP, unfinished

Etymology

I named Duchathair after the Irish stone fort Dún Dúchathair, which is located in Inishmore (Inis Mór). I came up with many central ideas for the language while wandering the ruins. Note that the language is spelled with the ú replaced by u. This is to differentiate it from the original location and to make it easier to spell with an English keyboard.

Implementation

Coming soon! (maybe)