Probabilistic Lambda Calculus: Beyond Deterministic Evaluation
Functional programs are inherently parallel, because sub-expressions can be evaluated in parallel; still, we can reason on a program using a deterministic sequential model, because the result of the calculus is independent from the evaluation order. This property ultimately relies on confluence of the lambda calculus.
It is well known that probabilistic lambda calculus is non confluent. The typical way out is to fix a deterministic reduction strategy. While we know that full reduction behave wildly, is there more structure to uncover between it and the extreme of a fixed deterministic strategy?
We present on-going work which is motivated –on one hand– by such a question, and the desire of better understand the issue behind non-confluence in the probabilistic setting, and –on the other hand– by a general observation: very little is known about the operational semantics of the probabilistic lambda calculus.
Tue 15 Jan
|09:00 - 09:30|
|09:30 - 10:30|
Matthijs VákárUniversity of OxfordFile Attached