Freude

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.

Freude structures

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 is Freude.

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.

Status of Freude.

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

The "object" structure.

So let's push the bottom most dictionary onto the stack of dictionaries.

      'object structure
    

The require Arrows for the "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
    

Definitions based on the the Arrows.

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
    

Logical Implication.

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
    

The Axioms of the "object" structure.

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

over
means copy the element one below the top of the stack onto the stack.
dup
Means duplicate the element on top of the stack.
rot
Rotates the top three elements of the stack, moving the third one down to the top.
swap
Swap the top two elements of the stack.

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
    

The "stack" structure.

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

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
    
Valid XHTML 1.0! SourceForge.net Logo