738 |
738 |
739 The first non-trivial step is to read off from the specification free-variable |
739 The first non-trivial step is to read off from the specification free-variable |
740 functions. There are two kinds: free-variable functions corresponding to types, |
740 functions. There are two kinds: free-variable functions corresponding to types, |
741 written $\fv\_ty$, and free-variable functions corresponding to binding functions, |
741 written $\fv\_ty$, and free-variable functions corresponding to binding functions, |
742 written $\fv\_bn$. They have to be defined at the same time since there can |
742 written $\fv\_bn$. They have to be defined at the same time since there can |
743 be interdependencies. Given a term-constructor $C ty_1 \ldots ty_n$ and some binding |
743 be interdependencies. Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$ and some |
744 clauses, the function $\fv (C x_1 \ldots x_n)$ will be the union of the values |
744 binding clauses, the function $\fv (C\_raw\;x_1 \ldots x_n)$ will be the union |
745 generated for each argument, say $x_i$, as follows: |
745 of the values generated for each argument, say $x_i$, as follows: |
746 |
746 |
747 \begin{center} |
747 \begin{center} |
748 \begin{tabular}{cp{8cm}} |
748 \begin{tabular}{cp{8cm}} |
749 $\bullet$ & if it is a shallow binder, then $\varnothing$\\ |
749 $\bullet$ & if it is a shallow binder, then $\varnothing$\\ |
750 $\bullet$ & if it is a deep binder, then $\fv_bn x_i$\\ |
750 $\bullet$ & if it is a deep binder, then $\fv_bn x_i$\\ |