===== vs synonyms

[unhan...@gmail.com]

On page 224 of tBoS you discuss a subtle difference between ===== and synonyms. I'm puzzled by your statement that the L rule

X:(list number)>>P;

___________________

X:numbers>>P;

is of no use in proving

(value *test*):numbers>>(head (value *test*)):number

I would have thought that since

_________________

X:(list number)>>X:(list number)

that the L rule would give

_________________

X:numbers>>X:(list number)

r code here...

after which the desired result follows by applying the rule for head.

I guess I'm probably misunderstanding the L rule, but maybe it's something deeper.

[Mark Tarver]

L rules generally only come into play when type checking functions.  The problem (head (value *test*)) : numbers just translates as 

Prove (head (value *test*)) : numbers.  

The context is empty. So the rule

X : (list number) >> P;

_______________________

X : numbers >> P;

is of no use.  

Mark

[unhan...@gmail.com]

So by "the context is empty" you mean that even the basic axioms of sequent calculus aren't available, e.g.

______________
P>>P

?

And if ===== is not a biconditional, can you explain intuitively what it does mean?

I can understand that for performance reasons it would be preferable to use synonym in this case, but that's not an option when defining a more complex type.  Is there any other situation in which ===== not being a true biconditional causes trouble?

[Mark Tarver]

============ is basically a shorthand (LR rule) for two rules - an L rule and an R rule where both the rules are symmetrical.

P; Q

======

(P & Q);

is shorthand for

P; Q;

_______

(P & Q);

and

P, Q >> R;

____________

(P & Q) >> R;

The other contexts where you see the difference is where you've used an LR rule to define the equivalence of types and want to see substitution carried out within any type parameter.  The LR rule will not in itself formally allow you to this but synonyms does.  In such cases you may need to work a little with some of your coding. You'll see an example of this in the discussion of subtypes; where an intuitively simple and elegant definition of subtypes has some corner cases based on this phenomenon.

Logically speaking an LR rule is not the same as an identity.  

By 'the context is empty';  I mean that the type checker approaches the problem with a zero set of hypotheses.  This does not mean that it has forgotten its type theory!

Mostly 

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[unhan...@gmail.com]

But in this particular case isn't the problem that the type checker doesn't know that

________________________________
X:(list number)>>X:(list number)

?

Or is the type checker denied access to the L rule in this situation?

Or perhaps I'm misunderstanding how the sequent calculus has been adapted for this purpose.

[Mark Tarver]

It's not denied access.  There just nothing in the formalisation to introduce this rule into the proof.  Yes of course it knows the rule you have cited - called hyp in Ll - but that rule doesn't help here.

Mark

--

[unhan...@gmail.com]

So the type checker is not a full blown theorem prover, it only draws very simple inferences. Thanks for clarifying.

[Mark Tarver]

I'm not sure what you mean by 'full blown'.  It cannot infer what doesn't follow from the way you formalise the problem.    

Mark

On Fri, Jun 9, 2017 at 11:20 PM, dabr...@indiana.edu <unhan...@gmail.com> wrote:

So the type checker is not a full blown theorem prover, it only draws very simple inferences.  Thanks for clarifying.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.

To post to this group, send an email to qil...@googlegroups.com.

[unhan...@gmail.com]

OK, would it be more accurate to say you haven't attempted to capture the full strength of the sequent calculus? 

[Mark Tarver]

The terms 'full blown' and 'full strength' don't apply to the sequent calculus.  They only apply to systems written in sequent calculus. 

Mark

On Sat, Jun 10, 2017 at 6:46 PM, dabr...@indiana.edu <unhan...@gmail.com> wrote:

OK, would it be more accurate to say you haven't attempted to capture the full strength of the sequent calculus? 

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.

To post to this group, send email to qil...@googlegroups.com.

[unhan...@gmail.com]

And your system is not full strength.

On Saturday, June 10, 2017 at 3:30:48 PM UTC-4, Mark Tarver wrote:

The terms 'full blown' and 'full strength' don't apply to the sequent calculus.  They only apply to systems written in sequent calculus. 

Mark

On Sat, Jun 10, 2017 at 6:46 PM, dabr...@indiana.edu <unhan...@gmail.com> wrote:

OK, would it be more accurate to say you haven't attempted to capture the full strength of the sequent calculus? 

--
You received this message because you are subscribed to the Google Groups "Shen" group.

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.

[Mark Tarver]

To make this clear.

1.  The concept of 'full strength' doesn't have meaning for SC.  It isn't a term of art that logicians know or understand.  There are concepts like soundness and completeness wrt a set of rules in SC and a proof procedure or soundness and completeness wrt a semantics. 

2.  Asserting LR equivalence is a weaker relation than identity.  

3.  There is a biased search in Shen based on Prolog which is sound and incomplete for certain kinds of problem but ....

4.  3. has nothing to do with what happens in p 224.  

Mark

To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.

[unhan...@gmail.com]

I realize "full strength" is not a "term of art", I was using it informally to mean as strong as standard FOL.

Regarding the type problem on p. 224, if the context is empty, then isn't there a sense in which the type checker doesn't know that

X:(list number)>>X:(list number)

?

Is there a reason you want the context to be empty?  The issue on p. 224 could be avoided by adding that single item to the context.  But perhaps it's not worth the overhead, and you'd rather encourage the use of synonym in this situation.

[Mark Tarver]

Hi,

Actually, that is partly down to you the user - as to whether the context remains empty.  Generally the context remains empty unless

a.  A function definition is type checked.

b.  The expressions contains an abstraction or a local assignment.

There is nothing to stop you adding an assumption to a context.  One could create a rule that said

(value *test*) : number >> P;

________________________

P;

However this is an example of an expansive rule - it can be applied to it's own output.  Hence this will cause an infinite loop.  You can get round this by clever use

of the cut to prevent '(value *test*) : number' being added repeatedly.   But most Shenturians prefer to just use the R rule.

Mark

--