TITLE: Scott's stochastic lambda calculi
QUESTION [19 upvotes]: Recently, Dana Scott proposed stochastic lambda calculus, an attempt to introduce probabilistic elements into (untyped) lambda calculus based on a semantics called graph model.  You can find his slides on line for example here and his paper in Journal of Applied
Logic, vol. 12 (2014).
However, by a quick search on the Web, I found similar previous research, for example, that for Hindley-Milner type system.  The way they introduce probabilistic semantics is similar to Scott's (in the former, they use monads while in the latter Scott uses continuation-passing style).
In which way is the Scott's work different from previous work available, in terms of theories themselves or their possible applications?

REPLY [15 votes]: One apparent strength of his approach is that it allows higher-order functions (i.e. lambda terms) to be observable outcomes, which measure theory generally makes quite tricky. (The basic problem is that spaces of measurable functions generally have no Borel $\sigma$-algebra for which the application function - sometimes called "eval" - is measurable; see the intro to the paper Borel structures for function spaces.) Scott does this using a Gödel encoding from lambda terms to natural numbers, and working directly with the encoded terms. One weakness to this approach may be that the encoding could be difficult to extend with real numbers as program values. (Edit: This is not a weakness - see Andrej's comment below.)
Using CPS seems to be primarily for imposing a total order on computations, to impose a total order on access to the random source. The state monad should do just as well.
Scott's "random variables" seem to be the same as Park's "sampling functions" in his operational semantics. The technique of transforming standard-uniform values into values with any distribution is more widely known as inverse transform sampling.
I believe there's just one fundamental difference between Ramsey's and Scott's semantics. Ramsey's interprets programs as computations that build a measure on program outputs. Scott's assumes an existing uniform measure on inputs, and interprets programs as transformations of those inputs. (The output measure can in principle be computed using preimages.) Scott's is analogous to using the Random monad in Haskell.
In its overall approach, Scott's semantics seems most similar to the second half of my dissertation on probabilistic languages - except I stuck with first-order values instead of using a clever encoding, used infinite trees of random numbers instead of streams, and interpreted programs as arrow computations. (One of the arrows computes the transformation from the fixed probability space to program outputs; the others compute preimages and approximate preimages.) My dissertation's chapter 7 explains why I think interpreting programs as transformations of a fixed probability space is better than interpreting them as computations that build a measure. It basically comes down to "fixpoints of measures are way complicated, but we understand fixpoints of programs pretty well."
{"set_name": "stack_exchange", "score": 19, "question_id": 25998}