283
edits
Work-in-progress: Difference between revisions
→Encoding lambda calculus in pipe-calculus
KalmanKeri (talk | contribs) No edit summary |
KalmanKeri (talk | contribs) |
||
| Line 22: | Line 22: | ||
\end{alignat} | \end{alignat} | ||
</math> | </math> | ||
The second step is normalisation. As translations utilize only a narrow fragment of PC, we can narrow down our term rewriting system too. | |||
<math> | |||
\def\rew{\mathrel{\Rightarrow}\,} | |||
\begin{alignat}{2} | |||
!s . t \rhd ?x . u \rew & t \rhd u[s/x] \\ | |||
\bot \rhd t \rew & t \\ | |||
s \rhd t \rew & \bot & \\ | |||
\end{alignat} | |||
</math> | |||
Substitution rules are exactly the same as in lambda calculus. | |||