 Axiomatic Language
started 3/5/2002; 10:21:00 AM - last post 3/11/2002; 11:40:46 AM
|
|
Walter Wilson - Axiomatic Language 
3/5/2002; 10:21:00 AM (reads: 743, responses: 2)
|
|
|
Axiomatic language is a pure logic programming language similar to Prolog. Its goals are (1) a pure specification language - "what, not how", (2) minimal, but extensible - small and simple but easily built up, and (3) a meta-language - able to simulate and thus subsume other languages. A smart translator, yet to be developed, would be needed to transform the specifications into efficient programs. The language is based on the idea that any computation, even an interactive program, can be represented by a static infinite set of symbolic expressions. Thus the language is just a simple formal system for generating symbolic expressions.
|
|
water - Re: Axiomatic Language
3/11/2002; 11:13:05 AM (reads: 760, responses: 0)
|
|
|
This sounds very similar to Maude which is an executable specification language based on concurrent equational term rewrite. It's also reflective: you can perform quotations and quasi-quotations, and in particular the rewrite semantics are a universal rewrite theory. This allows one to write a strategy specializer for your particular domain or logic (or even a strategy specializer for your strategy specializer ;) ). I know it's attracted John McCarthy's attention. There's a book on it called "Reflection in Rewriting Logic" which I own, and covers a lot of the major interesting points and application packages (which are very impressive). Unfortunately I can't seem to connect to the Axiomatic Language site, so I can't really compare them. :) I can say, though that Maude is free but not Free, which is regrettable. It started as a Lisp application and someday I am sure I will embed its semantics as an application into my own language.
|
|
water - Re: Axiomatic Language
3/11/2002; 11:40:46 AM (reads: 754, responses: 0)
|
|
|
I should add that the rewriting corresponds to a calculus of sequents, but also relates to evaluation. This is Yet Another epicycle of the Curry-Howard-deBruijn isomorphism between proofs and types, and predicates and terms.
|
|
|
|