Issue 86 in teyjus: adding spy turns a failure to a success

[tey...@googlecode.com]

Status: Accepted
Owner: dale.a.m...@gmail.com

New issue 86 by dale.a.m...@gmail.com: adding spy turns a failure to a
success
http://code.google.com/p/teyjus/issues/detail?id=86

When writing a program, I inserted some debugging calls into the code.
Inserting a "spy point" lead to the right behavior. When the spy point was
removed, the program failed to compute the correct answer.

The problem is described in more details in the attached .mod and .sig
files. This code is a reduced version of the context in which I found this
problem.

Specifics of my computing environment:

dale@dale-Latitude-6430U:$ tjcc -v
Teyjus version 2.0-b2

dale@dale-Latitude-6430U:$ uname -a
Linux dale-Latitude-6430U 3.5.0-45-generic #68-Ubuntu SMP Mon Dec 2
21:58:52 UTC 2013 x86_64 x86_64 x86_64 GNU/Linux

Attachments:
bug2.sig 537 bytes
bug2.mod 1.4 KB

--
You received this message because this project is configured to send all
issue notifications to this address.
You may adjust your notification preferences at:
https://code.google.com/hosting/settings

[tey...@googlecode.com]

Comment #1 on issue 86 by fafo...@gmail.com: adding spy turns a failure to
a success
http://code.google.com/p/teyjus/issues/detail?id=86

Actually you can aleady see the difference if you add a dummy
term_to_string instead of the "spy". The reason is term_to_string performs
head_normalization.

The conclusion is that somewhere there is a missing call to head_normalize
in the generated code. I'll investigate it but this may take longer than
spotting the problem...

[tey...@googlecode.com]

Updates:
Labels: Priority-Low

Comment #2 on issue 86 by fafo...@gmail.com: adding spy turns a failure to
a success
http://code.google.com/p/teyjus/issues/detail?id=86

I have a "solution".
Pattern matching against pi quantifiers should be like
pi x\ _
instead of
pi _
as you did.

Change it and then it works perfectly.
However I agree that the behavior should be the same in both cases (or
reject the pi _ syntax).
But I think as correctness is not impacted this bug should have a low
priority.

[tey...@googlecode.com]

Comment #3 on issue 86 by dale.a.m...@gmail.com: adding spy turns a failure

to a success
http://code.google.com/p/teyjus/issues/detail?id=86

Thanks for the easy work-around. I would prefer that we allow syntax such
as (pi G) and that this bug gets fixed eventually. I agree that it does
impact directly on correctness.

[tey...@googlecode.com]

Comment #4 on issue 86 by fafo...@gmail.com: adding spy turns a failure to
a success
http://code.google.com/p/teyjus/issues/detail?id=86

Actually what I proposed was not a work-around but the use
of another (related) bug:

In your example it works because
non_atomic (pi x\ _) does not match a term of the shape
pi w\ Z
with w free in Z.
(whereas it should)

You can try to replace
non_atomic (pi x\ _).
by
non_atomic (pi x\ Z x).
and it fails again (without the spy).

So far the best thing to do is to use your spy.
At least you have a correct result for correct reasons.


The original problem remains the absence of a normalization.
More than head normalization is needed since you need
to perform a beta reduction under your pi...

[tey...@googlecode.com]

Comment #5 on issue 86 by fafo...@gmail.com: adding spy turns a failure to
a success
http://code.google.com/p/teyjus/issues/detail?id=86

I will add a separate bug report to clarify things

[tey...@googlecode.com]

Comment #6 on issue 86 by fafo...@gmail.com: adding spy turns a failure to
a success
http://code.google.com/p/teyjus/issues/detail?id=86

Sorry I was wrong,

non_atomic (pi x\ _) does not match a term of the shape
pi w\ Z
with w free in Z.

and this is the expected behavior (since _ is implictly quantified above
the pi x) it cannot contain any x.