19
$\begingroup$

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?

Improve this question
$\endgroup$
1

1 Answer 1

Reset to default
15
$\begingroup$

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."

Improve this answer
$\endgroup$
6
  • 3
    $\begingroup$ Quick question: there are lot's of probabilistic process calculi. It's known that $\lambda$-calculi can be embedded precisely into process calculi (I'm simplifying a bit), following Milner's pioneering Functions as Processes. If we use Milner's techniques to embed a $\lambda$-calculus in a probabilistic process calculus, we get a probabilistic $\lambda$-calculus. What would be the relationship between that and Scott's approach? $\endgroup$
    – Martin Berger
    Commented Oct 10, 2014 at 9:12
  • 1
    $\begingroup$ @Martin: I really can't answer that quickly because I don't know much about process calculi, but it seems like it would be worth looking into. I'd be curious to know what the properties of the process calculi look like after transferring them over, and whether the transferred properties could be leveraged in any way. $\endgroup$
    – Neil Toronto
    Commented Oct 10, 2014 at 11:41
  • 2
    $\begingroup$ Every countably based $T_0$-space embeds in the graph model. Via this embedding we can then happily marry $\lambda$-calculus with topology and compute with, say, real numbers. The embedding is quite natural: a point is represented by the filter of its basic neighborhoods. $\endgroup$
    – Andrej Bauer
    Commented Oct 10, 2014 at 11:48
  • $\begingroup$ @Andrej: So extending the encoding with real numbers shouldn't be a problem, then? $\endgroup$
    – Neil Toronto
    Commented Oct 10, 2014 at 11:54
  • 1
    $\begingroup$ @NeilToronto Yes, it's an interesting subject. There is a large number of different process calculi, and several different ways of turning them stochastic. There are also different ways of encoding $\lambda$-calculus. The precise stochastic $\lambda$-calculus on arrives at by reflecting the encoding would depend on all these details. $\endgroup$
    – Martin Berger
    Commented Oct 10, 2014 at 13:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.