User:Junkshipp/Sandbox

Duchathair

Duchathair is a functional programming language inspired by PRA and theorem provers. Duchathair can be used to define functions and prove theorems about them.

Syntax

Whitespace and comments

The normal 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.

Calling functions

Duchathair essentially uses [Polish notation] for calling functions. So, instead of something like a * b, the notation used is times a b. All user defined functions, including multiplication, are [binary] (i.e. they take two arguments), so no brackets are needed to parse expressions. Additionally, there's a single unary operation, +, which denotes the successor of a number. While spaces are usually needed to separate different functions from their operands, such a space can be omitted between + and the operand.

In addition to calling a function, you can also call @function. This is the primary way recursion is implemented. You can think of @ as an operation that takes a function and executes it a specified number of times on an input. So, for example, if f x y = add x y, then @f x y. Actually this kinda doesnt work I have to make something more elegant.

Defining functions

The definitions of new functions take a form like the following:

example $ times y times x y

This line would define a new function which, when called with two arguments x and y, returns y*(x*y), assuming times is defined by the user as usual.

A function can only be defined once. Only previously defined functions can be used in new definitions. This means something impredicative like f $ f x y would be disallowed.

Instead, recursive functions are called using the @ symbol.

you can only use previously defined functions. you cannot define a function twice. defined functions must be all lowercase. x and y are reserved and annoy be used

Deduction

results have capital names they actually represent strings you can reassign a capital name to a different result principle: if a capital name represents some result, that result has already been proven

to assign a result to a name, create that result from previous results by a deduction (maybe giving it a function too) and then give a name you want to assign the result to

examples of deductions: [result] represents name corresponding to that result {function definition} represents name corresponding of that function rewrite this section to be clearer

[f 0 y = g +0 y] #xs [f x y = g +x y] {h $ 0};
also, #sw switches x and y around;
[h x y = 0] #df h;
[@h 0 y = y] #bs h;
[@h +x y = h x @h x y] #rc h;
[i x y = @h x y] #in [i 0 y = y] [i +x y = h x i x y];
[B = C] #eq [A = B] [A = C];
[a b 0 0 0 = a +0 0] #id [b 0 0 = +0] a;

Example code

The following code proves the commutativity of addition.

suc $ +y;
add $ @suc x y;
"the goal is to prove add x y = add y x";

radd $ add y x;
SUCB #bs suc;
SUCR #rc suc;
ADD #df add;
RADD #df radd;

o $ 0;

"let’s first try to prove radd 0 0 = 0";
ADDO #xs ADD o;
ADDOO #df;
wip

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