Freude is a postfix, concatenative, very strictly typed language in the style of Joy.
Objects in Freude are axiomatic mathematical structures. ie. collection of arrows (function signatures) and axioms.
Being a stack based language, there are no variables.
With the exceptions of arrows, (which have no implementation) the type signature functions are never specified by the programmer. I believe that is too error prone. Programmers often get it wrong. The type signature of any function is inferred by the Freude compiler from the definition, usually on the side of making things too concrete.
You are cannot state that any concrete implementation is a particular structure. You may merely suggest it to the compiler and the compiler will check whether the concrete implementation has the appropriate function signatures, and verify (not necessarily prove) that it obeys the axioms. (I aim for a pragmatic, rather than proof theoretic language.)
Think Design-By-Contract rather than program proving.
This document you are looking at is Freude.
It's written in XHTML so you can strip out the waffle leaving behind all the "pre" tags with class="freude". What is left is the code.
I'm still designing it and writing it. I have thought about it for years, but now I'm just starting to "put editor to xhtml" so to speak.
Text in this sort of box means "fixme". Anything in a "fixme" box I'm still thinking about how to make it right and any suggestions would be most welcome.
The following box is a bit of Freude code containing only comments.
; Freude inline comments look like this. Everything after
; a semi-colon until the end of
; the line.
The name comes from the fact that much of it is inspired by Manfred von Thun's Joy language, which indeed was a Joy to behold. And hence Schiller's Ode to Joy seems appropriate.
Everything is an object, so here we define an object.
Somewhen later I will formally define a structure as a structure.
(So long as there is nothing scary about a recursion, whose afraid of a little multi-level recursion?)
The structure of a structure is a list of arrows, followed by a list of definitions and then a list of axioms, then a name.
Oh yes, this is a postfix / stack based language. So instead of
writing something like 1+1=2 you write 1 1 +
2 equal Like Joy, Postscript, Forth or HP RPL.
The infix list notation used by Joy [a b c] is slightly
different in Freude.
The '[' operator means create a new stack. The ']' operator means bundle
everything on this stack into a list and push it onto the old stack.
'blah means the symbol blah, whereas blah means
the value of the symbol blah.
Here is the classic untidyness of quoting. In Lisplike languages "quotations" are done likes so...
(set (quote variable_name) value)
Which is often abbreviated to...
(set `variable_name value)
And even more so...
(setq variable_name value)
In Freude the "meta-character" single quote means the next thing is quoted, and not evaluated. For example...
'this_is_just_a_symbol '[this is just an unevaluated list of symbols]
I need to think a little (a lot?) more about the meaning of '[
Like Postscript, Freude has two stacks. A stack of objects, and a stack of dictionaries. Names are looked up in the top most dictionary. If it is not found there, the lookup process is repeated recursively in the next one down.
And arrow is the signature of a function.
For example the operation + over integers is a mapping of (ZxZ)->Z
We write that in Freude as
[integer] [integer integer] '+ arrow
So let's push the bottom most dictionary onto the stack of dictionaries.
'object structure
So here is the list of arrows require by objects.
Objects have a notion of equality.
[object] [object object] 'equal arrow
There is a unique object called the nil object. The later axioms will show that by nil we also mean "false". Anything other than nil is true.
[object] [] 'nil arrow
We have the notion of "or". As in logical or.
[object] [object object] 'or arrow
Lets define some handy functions using the above...
Not is simply the result of comparing with nil.
"define" pushes the little program in its first argument into the dictionary..
[ nil equal ] 'not define
This is the one anyone not use to symbolic logic will struggle with. If I fail to convince, read up on symbolic logic.
Traditionally A implies B is written
A => B
And has the meaning that if you assert that
A => B
Then you mean that if A is true, then B is true
Now counter to your intuition....
A => B
is equivalent to (not A) or B
Think about it, you assert A implies B.
Thus if you assert (not A) or B then
If A is false, your assertion is true AND if A is true, then
your assertion is true if and only if B is true.
Which is what you mean.
So in postfix land we write A => B as
B A implies
[ not or ] 'implies define
Of course we can use De Morgan's laws to construct "and" from "not" and "or".
[ not swap not or not] 'and define
Hokay, now we can start writing some axioms about how all this lot should behave.
Axioms are basically functions that always return true.
[ dup equal ] 'equals_is_reflexive axiom
Ooh! What's that "dup"? Well its stack manipulation stuff. I'll define it later. (So what is wrong with a wee bit of recursion hmm?)
Well, for just for us to work with now...
Note that there is something quite interesting going by in that
first axiom...
The axiom is a function from objects to
objects. The axiom is stating for all objects, it is true that
it is equal to itself. Note the "for all".
Instead of
having a quantification symbol like "for all", I merely state
that this function is true on its domain.
[ over over equal rot rot swap equal implies] 'equals_is_symmetric axiom
; a b c
[ over over ; a b c b c;
equal ; a b c (b=c)
rot4 rot4 ; c (b=c) a b
over ; c (b=c) a b a
equal ; c (b=c) a (b=a)
swap ; c (b=c) (b=a) a
rot rot ; c a (b=c) (b=a)
and ; c a (b=c and b=a)
rot rot ; (b=c and b=a) c a
equal ; (b=c and b=a) (c=a)
implies ; ((b=c) and (b=a)) implies c = a
] 'equals_is_transitive axiom
[ over over or rot rot swap or implies] 'or_is_symmetric axiom
[ dup nil or equal] 'or_with_nil_is_identity axiom
We have a stack. What does that mean? We can push things, pop things, dup things, swap things etc. etc.
We need the notion of swapping the top two elements!
[object object] [object object] 'swap arrow
Duplicate the object on top of the stack
[object object] [object] 'dup arrow
Drop the element on top of the stack.
[] [object] 'drop arrow
Rotate the top three items 1 2 3 rot is equivalent to 2 3 1
[object object object] [object object object] 'rot arrow
Duplicate the second item on the stack
[object object] [object object] 'over arrow
Some axioms to "say" what we mean by the above...
And here I have a wee conceptual difficulty... Is this an axiom for "dup" or an axiom for equal?
[dup equal] 'dup_duplicates axiom
"over" copies the element just below the top of the stack...
[;a b
over ; a b a
swap ; a a b
drop ; a a
equal] `over_copies_second axiom
"swap" swaps...
[ ; a b
over over ; a b a b
swap ; a b b a
rot rot ; a a b b
equal ; a a (b=b)
rot rot ; (b=b) a a
equal ; (b=b) (a=a)
and ] 'swap_swaps axiom
And rotate rotates...
[; a b c
over2 over2 over2 ; a b c a b c
rot ; a b c b c a
; AND A MIRACLE HAPPENS HERE!
] 'rotate_rotates axiom
I need to think about this one.... Functions are always single valued...
[;a b c
over over equal ; a b c (b=c)
rot rot ; a (b=c) b c
rot4; (b=c) b c a
dup rot rot; (b=c) b a c a
eval ; (b=c) b a a(c)
rot rot eval ; (b=c) a(c) a(b)
equal ; (b=c) ((a(c)=b(c))
implies] 'functions_always_return_same_value
Natural numbers have two notions, zero and next....
'natural_number structure
[natural_number] [] 'zero arrow
[natural_number] [natural_number] 'next arrow
Zero is not the successor of anything...
[next zero equal not] 'zero_not_successor axiom
"next" is one-to-one. ie. If a and b are not equal, then
next(a) != next(b)
[; a b
over over ; a b a b
next ; a b a ++b
swap next; a b ++b ++a
equal ; a b (++b ++a =)
rot rot equal ; (++b ++a =) (ab=)
implies ; (++b == ++a) => (a == b)
] 'next_is_one_to_one axiom
|
|
|