Original QTT Erasure algorithm

Original QTT Erasure algorithm

Disclaimer This text only explains the QTT Erasure algorithm, you must already be familiar with how QTT works.

Initially, the algorithm assumes that:

• any typechecked term $t : \rho > T$ elaborates to a program p¹;
• $\rho \neq 0$, since you want to make sure that your program actually has something to execute before translating it into runnable code;
• the translation is into the untyped $\lambda$-calculus.

The whole algorithm traverses the tree of terms elaborating programs – given that dependent types are the zero resource being erased. For a more complex language, we should probably not merge QTT erasure with an actual elaboration phase.

The only terms affected by erasure are binding-dependent terms, in McBride’s calculus, it’s $\lambda$ abstraction and application.

The algorithm goes as follows:

• for $\lambda$-abs with a zeroed resource,
  • you have a variable $0 > x : S$ ² bound to a body $\rho t : T$;
  • it elaborates to a program p of type $T$. Meaning, that $x$ won’t be consumed in p – as it was evaluated already – and, then, $p$ can proceed.
• for $\lambda$-app with a zeroed resource,
  • you have a function $f$ that takes a variable $0 x : S$;
  • while within your context, you have a zeroed value $s : S$;
  • given $f[s : S/x]$, p elaborates to the body $t : T$ of $f$. Meaning that what’s left for $f$ is the returning function when $s$ is applied.
  • for all remaining terms, elaborate it as is.

The main idea of the paper is to pre-bind zeroed resources, making it unavailable to the elaborated program p. The main trick of the paper is to pair zeroed resources from $\lambda$-abs with zeroed resources from $\lambda$-app. McBride’s paper provides a proof that a zeroed application will always meet a zeroed $\lambda$ abstraction.

Resources

1. I Got Plenty o Nuttin by Conor McBride