EXTENDED HEREDITRY HARROP FORMULAS in LINEAR LOGIC:
     Nothing but an Interpreter called Helmet - by G. Delzanno -
------------------------------------------------------------------------------

HELMET  represents a further step towards the definition of a 
logical environment in which specifying complex programming features
aided by automated-deduction systems a la Prolog.
The interpreter presented here is based on a subset of Forum called Ehhf 
in which non-determinism is reduced to multiple-headed clause selection.
The code is in the file:

 - sig.mod, helmet.mod 

A parser for Ehhf formulas: parser.mod

DESCRIPTION:

Ehhf is an extension of Prolog with multiple-headed clauses:
Goals have the form: 
?- ehhfsolve Ops.
where Ops is  (Op1 | ...| Opn ) and Opi can be:

 - an atomic formula A,
 - (pi G)  i.e., forall G
 - G1 & G2
 - D -o G   D a clause (when instantiated)
 - D => G     "   "  
 - anti 
 - all 
  
A current state is kept by the interpreter (a multiset of atomic formulas)
Its initial value must be set with the predicate "initial", e.g.,

initial  anti.      % empty
initial  (p "Carl" | p "Joe"). 
 
There are 4 types of extended clauses:

Cond >> Head || State --> Ops || NState.

Head, State, NState have the form (A1 |...|An) with Ai an atomic formula

It rewrites the current goal G and the current state S in accord with the 
pair Head || State (i.e., by selecting a subset of G,S which UNIFIES* with 
Head,State) of the clause into its body Ops || NState if Cond succeeds. 
Cond is a conjunction of standard lambdaProlog predicates. 
* higher-order unification. 

Cond >> Head || State.

It succeeds if the current goal and the current state match exactly 
with the pair Head || State and  Cond suceeds.

Head || State --> Ops || NState
Head || State.

The same as above without any extra condition.

It is also possible to write clauses like:

Cond >> Head || State --> Body || NState:- 
 Constraints.

where Constraints are invocation of standard lambdaProlog predicates.

See the draft enclosed for more details.

A simple example: a specification of a counter

module count.
import helmet.  % to import the interpreter!
type counter  o.
type start    o.
type add      int -> int -> o.

add C C1:- C1 is C+1.
 
add C C1 >>
  inc || counter C -->  anti || counter C1.

% anti must be always used when there are no elements in one of the 
  components of the clause. 

new counter || anti --> anti || counter 0.

initial anti.
start:- ehhfsolve (new counter | inc | inc).

EXAMPLES:

We present different examples of specification like: 

1) Concurrent Object-Oriented Programming:   
   -   obj.mod,    fact.mod 

Usage (in the -.rc file):
 
 #load "sig.mod"
 #load "helmet.mod" 
 #load "obj.mod"
 #load "fact.mod"
 #query fact.
 start. 

   -   objone.mod, objample2.mod 

Usage (in the -.rc file)
 
 #load "sig.mod"
 #load "helmet.mod" 
 #load "objone.mod"
 #load "objample2.mod"
 #query objample2.
 start. 

2) Code Mobility
   -   mobile.mod  

Usage (in the -.rc file)
 
 #load "sig.mod"
 #load "helmet.mod" 
 #load "mobile.mod"
 #query mobile.
 start. 

3) Concurrent transactions
   - spec.mod 
Usage (in the -.rc file)
 
 #load "sig.mod"
 #load "helmet.mod" 
 #load "spec.mod"
 #query spec.
 start. 

4) State-based 
   - prog.mod

Usage (in the -.rc file)
 
 #load "sig.mod"
 #load "helmet.mod" 
 #load "prog.mod"
 #query prog.
 start.