Commit 10af280e authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents ab90d60c 16053185
......@@ -96,6 +96,22 @@ The thesis is available at https://pnwamk.github.io/docs/dissertation.pdf
>> Mickael: premier draft et comparison avec worra
**ANSWER:**
The application inversion function from Kent's thesis is supposed to compute exactly the same type as our *worra* operator. However, we believe that there is a mistake (typo?) in its algorithmic definition (p108 fig 5.2).
Indeed, the formula of \tau_a seems incorrect: we think the first union should be an intersection.
Here is an example for which the current definition seems unsound:
```
inv (((True->False) /\ (False->True)) \/ ((True->True) /\ (False->False)), True)
= Bool \ (True\/False) = Empty
```
However, a function with a type `((True->False) /\ (False->True)) \/ ((True->True) /\ (False->False))` could definitively give a result in `True`. The correct result should be `Bool`.
If we change this union into an intersection, then Kent's formula becomes equivalent to our algorithmic definition of *worra* (p13) with a simple application of De Morgan.
**(END OF ANSWER)**
### Formal connections to prior work
......@@ -180,6 +196,18 @@ seem unneeded:
tests and have never seen this pattern.
>> Mickael: tu t'en occupes
**ANSWER:**
We agree with the reviewer on the fact that interdepedent tests do not seem to appear in real examples. The exemple we give page 6 to justify the need of interdependent tests is specifically built for this purpose and we did not find this pattern in the real examples we studied.
Still, in a theorical point of view, we think that it is important to notice the existence of interdependent tests. It helps to understand why the parameter `n_0` introduced in the algorithmic type system is required for the completeness. In a sense, it is similar to the use of type schemes in our algorithmic type system: it makes our algorithmic type system more complex but also more complete regarding to the declarative one.
Then, once these formal results have been established and that the role of type schemes and `n_0` are understood, we can choose to include it or not in a practical implementation depending on our needs. The remark of the reviewer seems to imply that a value of `n_0 = 1` is enough in practice, and we agree with this.
>> Maybe we should add this remark in the paper? We already say that choosing `n_0 = 2*depth` seems enough, but we could also say that `n_0 = 1` is enough in most cases.
**(END OF ANSWER)**
This paper makes a number of significant advances, which are somewhat
obscured by the complexity.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment