ann: S 41

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

This is a new release that folds in the changes introduced in the unreleased 40.1 and adds expressive power to the sequent calculus compiler.   The following improvements have been made over S 40.

1. Reduced code size (40.1).  The new code for the compiler is shorter, clearer and easier to maintain.

2. Better Prolog code emitted by the compiler (40.1).   This is pretty marginal TBH but it is faster.

3.  Increased expressive capacity wrt context variables.   This means that S 41 is featuring an aspect that is part of sequent calculus but hitherto not reflected in Shen.  This involves a single extra form of side condition.

4.  Capacity to place failure points in sequent rules.

The last two points require some explanation and I'll do this soon.  But S 41 takes less code but delivers more horsepower than S 40.   Download in the usual place.

M. 

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

OK; let's review the new features.

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;)

M.