search

google-code-export / omega

Automatically exported from code.google.com/p/omega
Other
2 stars 0 forks source link

(DiffLabel m n) is not usable as a proposition #67

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. load this file:
<http://omega.googlecode.com/svn/trunk/work/StaticFreeEnv.prg>

view it as 
<http://code.google.com/p/omega/source/browse/trunk/work/StaticFreeEnv.prg?spec=
svn235&r=235>

2. observe diagnostic:
In the theorem 'Mehr' the type:
   DiffLabel 'a 'b -> Free 'a 'c -> Free 'a {'b='d; 'c}r
is neither a back-chaining nor a left-to-right rewrite rule.
because the following are not propositions:
   DiffLabel 'a 'b
Thus, no rule is added.

3. observe test7; it is a negative test and passes. It should not, because 
test7 is statically well-formed. If I make it a positive test I get:
While type checking: test7
Under the truths: 
We tried to solve: Free `a {`b=Char,`a=[Char]}r,Free `b {`a=[Char]}r
But we were left with: Free `b {`a=[Char]}r, Free `a {`b=Char,`a=[Char]}r
The proposition: (Free `b {`a=[Char]}r) is refutable.

The proposition is only refutable because the back-chaining rule has not been 
added!

What is the expected output? What do you see instead?

Explained above. (DiffLabel a b) should qualify as a proposition.

Original issue reported on code.google.com by ggr...@gmail.com on 4 Aug 2009 at 9:57

GoogleCodeExporter commented 9 years ago 
Tim suggested to just change in the predefines
"data DiffLabel" to "prop DiffLabel" and see what happens. Unfortunately it did 
not work, see r236.

But I think that we can add a new Axiom (rewrite rule) like this:

Axiom (DiffLabel): ['a /= 'b] => DiffLabel 'a 'b --> []

This means we have to introduce non-equality constraints with all their axioms.

Original comment by ggr...@gmail.com on 5 Aug 2009 at 8:05

GoogleCodeExporter commented 9 years ago 
Okay, I have branched:
  branches/issue-67
contains a first attempt.

DiffLabel now automatically adds an axiom:

Axiom (DiffLabel): [] => 'a != 'b --> []

actually this should read:

Axiom (DiffLabel): ['a != 'b] => DiffLabel 'a 'b --> []

which means that (DiffLabel 'a 'b) can be immediately discharged if the tags 
differ.

I am working on this next.

NB.: The branch is very messy, and contains many hacks to appease the compiler, 
even if they are semantically 
invalid.

Original comment by ggr...@gmail.com on 8 Aug 2009 at 2:04

GoogleCodeExporter commented 9 years ago 
Since Label is an atomic singleton type, it is either 'Label <fixed>' or 'Label 
a', i.e. universally quantified.

Here is another plan: to check whether 'DiffLabel a b' is a true proposition we 
freshen it (so that we do not poison our world) and unify a and b. If that 
fails, we have a proof of the difference. If not, the unifier is the refutation.

N.B. I hear some constructionists murmuring "DiffLabel a b -> ⊥"

Original comment by ggr...@gmail.com on 8 Sep 2011 at 9:33