Implementation of Beyond Lisp

Currently I am trying to implement the idea that I have which is outlined at Beyond-lisp-notes . Basically I will add the mu special form to the scheme language. This will take a formal logic expression and see if it holds true for a computer program. The syntax we will use is an automated theorm prover in first order logic. I am also thinking of adding mu-let which would take a set of mu statements and prove if they hold true given a set of data.

Requirements

The software package will require gandalf to be compiled on your unix machine. There is a windows binary that I will make available for windows computers. It will also require scsh because I am programing the program in that scheme environment. The Gandalf package is independant of implementation since it creates its own binaries.

Scsh
Gandalf

Informal proof of application of the theory of groups to computer programs.

First we take a binary operation we call our computer program. A binary operation in groups can be any abstract thing. This abstract thing is founded upon the idea of In this proof we use the binary operation as the evaluation of a computer program. Closure can be proven in the computer program by the simple fact that anything evaluated by the computer returns a value that is specified inside of the definition language. Here is an excerpt from my paper on the subject.

A informal definition of a Group which is a set of axioms that has closure, associativity , identity and inverse. Closure can be reasoned by given two functions the output is always something that the program could reason as an output which is provided by the language the program is programmed in. Associativity could be reasoned by taking the output of one program and then taking that output and evaluating that output into another function. Inverse can be reasoned with a program that returns the output given the input. Lastly there is a program that returns the identity of the function. This would be quotation of the function and then evaluating the quotation. We use first order logic to confirm these hypothesis's given a computer program and this hypothesis will prove that a set of instructions is a group.

Beyond Lisp

I have been working on a idea from John McCarthy's lecture on Beyond Lisp for awhile. There is now a wiki page up that discusses the idea (See links). It basically adds a new operator to lisp that allows you to reason using formal logic with a computer. It reasons on both inputs and outputs on the computer program. The next few posts will be outlining operators to the scheme programming language to extend it to allow for McCarthy's ideas. For more information see the links at the bottom of the page

Links
Beyond-lisp
ILC Confrence Lecture Description

My Journey To Scheme

I had been wanting to program for awhile. Since I was very little of course when I was about 10. I started off with Visual Basic which is such a depressing programming language. I lamented in a great deal of depressing programming languages for awhile. From VB to Java to HTML to javascript and the list would go on almost indefinitely. Until one fateful day I discovered lisp. The odd syntax really made me wonder what it was and how to program in it. After awhile I started to understand scheme and really got into learning it. It wasn't a depressing programming language at all but an elegant one. Something I hadn't seen in a programming language when I started learning it. For example lets compair two programs in scheme and Java.

Java Programming language

 
public class Hello {
    public static void main(String[] args) {
        System.out.println("Hello, world!");
    }
}

Scheme Programming language

(display "Hello World")

As you can see both are quite different. For example scheme uses prefix notation with parenthesis while Java uses a C like syntax. Also Java forces a object oriented system down your throat. The advantage to a prefix notation is that it is easly understood what does what. Display acts upon the argument "Hello World" and displays it. Java on the other hand makes you use the object system integrated in the language. That is one of the reasons that the Java program is much larger. This doesn't mean that Scheme can't have an object system but it could possibly have.