1
$\begingroup$

I'm studying the Principal Type (PT) Algorithm in Basic Simple Type Theory by J. Roger Hindley. One step to find the PT of a term is the Unification of types. The Robinson's Unification Algorithm uses a comparison procedure like as follow:

Comparison Procedure

Given a pair $(u, v)$ of types, write $u$ and $v$ as symbol-strings, say

$u \equiv s_1 ... s_m$ and $v \equiv t_1 ... t_n$ $(m, n >1)$

where each o f $s_1,... , s_m$, $t_1, ... , t_n$ is an occurrence of a parenthesis, arrow or variable.

If $u \equiv v$, state that $u \equiv v$ and stop.

If $u \not \equiv v$, choose the least $p < \min(m, n)$ such that $s_p \not \equiv t_p$; it is not hard to show that one of $s_p$, $t_p$, must be a variable and the other must be a left parenthesis or a different variable. Further, $s_p$ can be shown to be the leftmost symbol of a unique subtype $u^*$ of $u$. (If $s_p$ is a variable, $u^* \equiv s_p$.) Similarly $t_p$ is the leftmost symbol of a unique subtype $v^*$ of $v$. Choose one of $u^*, v^*$ that is a variable and call it $a$. (If both are variables, choose the one that is first in the sequence given in Definition 2A1.) Then call the remaining member of $(u^*, v^*)$ $\alpha$; the pair $(a, \alpha)$ is called the disagreement pair for $(u, v)$.

My issue is with the Note bellow:

3D5.1 Note To prove that $p$ exists in the case that $u \not \equiv v$ in the comparison procedure we must show that it is not possible to have

$t_1 ... t_n \equiv s_1....s_m t_{m + 1} ... t_n$

with $n > m$. This is left as a (rather dull) exercise for the reader.

I disagree with this note. I can image, say, $u \equiv a \rightarrow b$ and $v \equiv a \rightarrow b \rightarrow c$, where no $p$ is possible.

Maybe I'm missing something! How $p$ is always possible?


As asked, the definition of types is given as follow:

2A1 Definition (Types) An infinite sequence of type-variables is assumed to be given, distinct from the term-variables. Types are linguistic expressions defined thus:

i. each type-variable is a type (called an atom);

ii. if $\delta$ and $\rho$ are types then $(\delta \rightarrow \rho)$ is a type (called composite type).

2A1.1 Notation Type-variables are denoted by "a", "b", "c", "d", "e", "f", "g", with or without number-subscripts, and distinct letters denote distinct variables unless otherwise stated.

Arbitrary types are denoted by lower-case Greek letters except $\lambda$.

Parentheses will often (but not always) be omitted from types, and the reader should restore omitted ones in such a way that, for example,

$\rho \rightarrow \sigma \rightarrow \tau \equiv (\rho \rightarrow (\sigma \rightarrow \tau))$

This restoration rule is called association to the right.

$\endgroup$
  • $\begingroup$ Check the formal definition of "types". What's the corresponding grammar? Are you sure that $a \to b \to c$ is a valid type in that grammar? (as opposed to $(a \to b) \to c$ and $a \to (b \to c)$) Can you include that grammar in the question? I suspect the proof of the Note will require reasoning about the syntax of types. $\endgroup$ – D.W. Jan 23 '17 at 17:53
  • $\begingroup$ @D.W. No formal grammar is given for the syntax of types in the book. But I will include the definition of types as is given. In advance I can say that types are right associative and parenthesis may be omitted. $\endgroup$ – Rafael Castro Jan 23 '17 at 18:02
  • $\begingroup$ @D.W. I believe you made a good point. My example seams not work with obligated parenthesis. Say, $u \equiv (a \rightarrow b)$ and $v \equiv ((a \rightarrow b) \rightarrow c)$ or $v' \equiv (a \rightarrow (b \rightarrow c))$. $p$ exists in both cases. $\endgroup$ – Rafael Castro Jan 23 '17 at 18:21
1
$\begingroup$

It looks like the answer is that, to be syntactically valid, composite types must be fully parenthesized.

In particular, $a \to b \to c$ is not a syntactically valid type (per definition 2A1). 2A1.1 introduces "syntactic shorthand": when they write something like $a \to b \to c$, it should be understand that they actually mean $(a \to (b \to c))$.

The Note appears to be valid when we restrict to syntactically valid types. Thus, your example is not actually a counterexample.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.