1: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
2: % about eta
3: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
4:
5: In the definition given in \cite{}, the rewrite relation which was
6: considered was the union $\a_\b \cup \a_\e \cup \a_\cR$. Now, the rule
7: $\b$ is not seen as a special rule: it is part of $\cR$. But, what can
8: we say about $\e$ ? Since rule left-hand sides must be headed by
9: function symbols, it is not possible to consider the rule
10:
11: \begin{center}
12: $[x]@(Z,x) \a Z$
13: \end{center}
14:
15: On the other hand, it is always possible to extend the alphabet with
16: symbols $\l_{s,t} \in F_{s\a t, s\a t}$, and restrict the set of terms
17: to the terms whose subterms of the form $[x]u$ are always headed by
18: some $\l_{s,t}$. Such a set is clearly stable by reduction.
19: Furthermore, since the type indices $s,t$ may be recovered by doing a
20: type analysis, they may be dropped. Hence, by writting
21: $\l_{s,t}([x]u)$ simply $\l x.u$, we recover a more usual syntax and
22: the rule
23:
24: \begin{center}
25: $\l x.@(Z,x) \a Z$
26: \end{center}
27:
28: \noindent
29: may be part of $\cR$. Thus, it is possible to include $\e$ in $\cR$,
30: if one restricts oneself to the set of terms described above.\\
31:
32: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
33: % lambda-extension
34: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
35:
36: A second kind of IDTS will also interest us, but rather for applying
37: Nipkow's higher-order critical pair technique for proving local
38: confluence in Section~\ref{}.
39:
40: \begin{dfn}[$\l$-extension]
41: The {\em $\l$-extension} of an IDTS-alphabet $\cA = (\cB, \cX, \cF,
42: \cZ)$ is the IDTS-alphabet $\l\cA = (\cB, \cX, \cF', \cZ)$ where:
43: \begin{lst}{--}
44: \item $F'_{s_1, \ldots, s_n,s} = F_{s_1, \ldots, s_n,s}$ if $n \neq 1$
45: or else $s_1 = s = t_1 \a t_2$,
46: \item $F'_{s\a t, s\a t} = F_{s\a t, s\a t} \cup \{ \l_{s,t} \}$.
47: \end{lst}
48:
49: \noindent
50: Then, the set $\l\cI(\cA)$ of {\em $\l\cI(\cA)$-terms} is the subset
51: of $\cI(\cA)$-terms whose subterms of the form $[x]u$ are always
52: headed by some $\l_{s,t}$. Given a $\cI(\cA)$-term $u$, we denote by
53: $u^\l$ the $\l\cI(\cA)$-term obtained by adding $\l_{s,t}$ above each
54: subterm of $u$ of the form $[x]v$.
55:
56: \noindent
57: The {\em $l$-extension} of an IDTS $\cI = (\cA, \cR)$ is the IDTS
58: $\l\cI = (\l\cA, \l\cR)$ where $\l\cR = \{ l^\l \a r^\l ~|~ l\a r \in
59: \cR \}$. Finally, we say that an IDTS is a {\em $\l$-IDTS} if it is
60: the $\l$-extension of some IDTS.
61: \end{dfn}
62:
63: Since $\l\cI(\cA)$ is stable by reduction, $\l$-extensions enjoys the
64: following properties:
65:
66: \begin{lem}
67: $\cI$ is strongly normalizing (resp. confluent, locally confluent)
68: iff $\l\cI$ is strongly normalizing (resp. confluent, locally
69: confluent) on $\l\cI$-terms.
70: \end{lem}
71:
72: As in the case of $@$, it is possible to drop the type indices. And
73: since, in a $\l\cI$-term, every subterm of the form $[x]u$ is headed
74: by some $\l_{s,t}$, it is possible to write it $\l x. u$. By this way,
75: the syntax of $\cI$ and $\l\cI$ are quite similar: $[x]u$ is merely
76: replaced by $\l x.u$.
77:
78:
79:
80:
81: %%% Local Variables:
82: %%% mode: latex
83: %%% TeX-master: "main"
84: %%% End:
85: