We study encodings of the lambda-calculus into the pi-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider lambdafail, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider spi, a pi-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of lambdafail into spi and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in lambdafail via typed processes in spi. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols.

翻译：我们研究了在尚未探索的带非确定性与失败的计算场景中，将λ-演算编码为π-演算的方法。在顺序计算方面，我们提出了lambdafail——一种新型非确定性演算，其中交集类型控制资源（项）；在并发计算方面，我们考虑了spi——一种基于线性逻辑与会话类型之间的Curry-Howard对应关系实现非确定性与失败的π-演算。我们给出了lambdafail到spi的类型化编码，并证明了其正确性。该编码通过spi中的类型化过程精确解释了lambdafail中非确定性与易错评估的相互作用，特别展示了顺序评估中的失败（资源缺失/过剩）如何被优雅地编码为交互协议。