equal
deleted
inserted
replaced
131 \end{center} |
131 \end{center} |
132 |
132 |
133 \noindent |
133 \noindent |
134 where the $x_i$ are bound in $s$. In this term we might not care about the order in |
134 where the $x_i$ are bound in $s$. In this term we might not care about the order in |
135 which the $x_i = t_i$ are given, but we do care about the information that there are |
135 which the $x_i = t_i$ are given, but we do care about the information that there are |
136 as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$ |
136 as many $x_i$ as there are $t_i$. We lose this information if we specify the |
137 as something |
137 $\mathtt{let}$-constructor as something like |
138 |
138 |
|
139 \begin{center} |
|
140 $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$ |
|
141 \end{center} |
|
142 |
|
143 \noindent |
|
144 where the $[\_].\_$ indicates that a list of variables become bound |
|
145 in $s$. In this representation we need additional predicates to ensure |
|
146 that the two lists are of equal length. This can result into very |
|
147 elaborate reasoning (see \cite{BengtsonParow09}). |
|
148 |
139 |
149 |
140 |
150 |
141 |
151 |
142 |
152 |
143 Contributions: We provide definitions for when terms |
153 Contributions: We provide definitions for when terms |