Content deleted Content added
just make it all lowercase |
see also pcf |
||
Line 27:
The CBN translation produces CBPV computations for each expression. A CBN function <code>λx.M</code> : <math>A \to B</math> translates unaltered, <code>λx.M<sup>N</sup></code> : <math>(U A^n) \to X^n</math>. A CBN application <code>M N</code> : <math>C</math> is translated to a computation <code>M<sup>v</sup> (thunk N<sup>v</sup>)</code> of type <math>C^n</math>. A pattern match <code>match V as { (1,...) in M_1, ... }</code> is translated similarly to CBN as <code>V<sup>n</sup> to z in match z as { (1,...) in M_1<sup>n</sup>, ... }</code>. ADT values are wrapped with <code>return</code>, but <code>force</code> and <code>thunk</code> are also necessary on internal structure. Levy's translation assumes that <code>M = force (thunk M)</code>, which does indeed hold.<ref name="Levy99"/>
== See also ==
* [[Programming Computable Functions]]
== References ==
| |||