ann: S 41.1 (for real)

[dr.mt...@gmail.com]

S41 was announced in February and then delayed by the hiatus
of being ill.  Consequently S40 has been the latest version until
the release of S41.1 which is now on the download site.

Bug Fixes
_________

(define foo
   {--> (list number)}
    -> (input+ (list number)))
   
failed under S40 and works under S41.1.

Recoding
_________

The sequent calculus compiler is shorter (S40, 286 lines; S41.1, 257 lines).
To repeat what I said in February the new compiler has features missing
from the old.

New Features
_____________

Despite being smaller the new compiler has features not in S40.

1.  Addition of fail as a primitive.

(datatype not

 X : A; !; fail;
 _______________
 X : (- (not A));
 
 _______________
 X : (- (not A));)
 
 You can write this in S40 and it will work 8 : (not symbol) etc.
 But fail has no recognised semantic role.  S40 will try to prove
 fail sadly.  S41 does not.
 
 2.  Context Variables.
 
 You get these in sequent calculus though mostly they are suppressed.
 
 P, Q,  D  |- R
 _________________
 (P & Q),  D  |- R
 
 Here  D  stands for the hypotheses other than (P & Q).  Mostly
 of course you don't need the  D  - we don't here - and we omit it.  
 That's why S40 et al. work so well; we mostly don't need it.  
 But S41 gives you the power to grab the context through one
 extra side-condition ctxt followed by a variable X.
 
 There are two possibilities wrt X.  Either A. it is fresh or B. it
 has been introduced prior in the deduction rule.    If A. X
is bound to the list of assumptions and listed as a context variable.
If B. it is listed as a context variable.
 
 Take this deduction rule

where  D* results from  D by removing all duplicated hypotheses  
D* |- P
D  |- P

In S41

(datatype no-dups

  ctxt D                                \\  Grabs the list of assumptions because D is fresh in the rule.
  let D* (remove-duplicates D)      \\  Bind D* to the result of removing all duplicates in D
  if (not (= D D*))                   \\ Check to see something happened (stops an infinite loop)
  ctxt D*                                 \\ Declare D* a context variable; 

                                               \\ because D* is not fresh it is simply listed as a context variable
   D* >> P;                                           \\ prove P with the thinned context D*
   _______
   P;)
   
 New Installation
 _________________
 
 S41.1 allows the user to choose which packages to load into the image
 above the bare kernel including Shen/tk and the IDE.  There is only
 one installation program (S40 had two).
 
 Mark