Bridging the informal and the formal

I'm doing work on designing languages for probabilistic reasoning.

In probability theory, it seems that random variables play the part of a bridge between the informal and the formal. They are defined as functions

Z : Omega -> S

where Omega and S are "sample spaces" (sets that can be quantified by probability measures). Formally, Omega and S are both well-defined. In practice, Omega seems to be regarded as the set of all possible realities, which Z can operate on and return formal values in S. (It seems that it has to be, or probability users couldn't use probability theory to theorize about real-world phenomena.)

I was recently reading Olin Shivers's excellent dissertation, in which he states that free variables can be seen as bridging the informal with the formal. In other words, a program that consists of just an identifier "x" (assuming valid programs can have free variables) can be taken as meaning

x  ; to be changed later by some external, informal process

or that the context of "x", which "x" will be embedded in later by an external process, will determine its value.

I'm interested in explaining random variables in familiar terms. Besides Shivers's observation, I've had I/O functions suggested. What have you come across that can be regarded as bridging the informal and the formal?

Neil T

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Probabilistic Functional Programming

Martin Erwig's page on Probabilistic Functional Programming and Probabilistic Functional Programming in Haskell, Martin Erwig and Steve Kollmansberger, Journal of Functional Programming, Vol. 16, No. 1, 21-34, 2006.

I also read Stochastic Lambda Calculus and Monads of Probability Distributions by Norman Ramsey and Avi Pfeffer 7 or 8 years ago, and rather liked it.

Embedded probabilistic functional programming

Perhaps you might like a probabilistic programming language that is
fully developed, has lots of libraries and the efficient
compiler. That language is OCaml. Deterministic computations are
written as they are normally written in OCaml. In addition, we can
specify generative graphical models as non-deterministic computations,
with the help of a library function dist. We can also write exact
inference procedures and importance sampling, also in
OCaml. Furthermore, a model may itself invoke an inference procedure
(after all, it is just an OCaml function). We thus obtain nested
inference and distributions parameterized by distributions.

Please see the following message for more details on our library
(developed with Chung-chieh Shan)

http://caml.inria.fr/pub/ml-archives/caml-list/2009/06/6f9b53a503ca9c18ff24ef4275b87685.en.html

The two papers referenced in the message might be of interest too.
One of them will be presented in two weeks at UAI. Currently we deal
with discrete distributions; we are interested about continuous
ones. We need to find a good example first.

IBAL

There's also Avi Pfeffer's IBAL language.

Probabilistic languages were

Probabilistic languages were discussed here several times. Search the archive.

I know they've been discussed

I probably posed my question wrong, seeing as how everyone misunderstood it. I think I took too long to get to the point. For heck's sake, I even blindsided Ehud.

I have searched the archives, and I am already familiar with PFP, IBAL, and probability monads, in addition to quite a few other languages, libraries, and nifty bits of research. (Thanks for taking the time to link to those, everyone.) Oleg, I think I've seen your embedded stuff before in a TR, but I hadn't seen the other papers - so thanks for the link.

Second try: I'm looking for PL analogies so I can explain a probability concept, or draw on the analogies for inspiration. I want other instances of bridges between the formal and the informal. I've already got I/O functions and free variables that can do that, and I was wondering if there were more that any of the brilliant people here could identify.

If I understand correctly,

If I understand correctly, whenever we reify a notion -- a continuation for the rest of the computation, a FRP/dataflow variable for the lifetime of a location, etc. -- we are doing this. The rough concept might be there, but a lot of power can be gained from making it explicit and part of the system. In the above cases, it is easier to analyze and optimize code.

Generally, we have property in a library or program analysis, and as we determine it is more and more important, often make it a second class citizen, and, ultimately, perhaps a first class or implicit one.

clarity...

Does the phrase "bridge between the formal and the informal" mean "place where the code accepts input that may not be from a well-defined source"? i.e. where the semantics of the program cannot or do not express the range or distribution of values that may be injected there?

Random variables in Haskell

I'm interested in explaining random variables in familiar terms.

I'm not sure if it really address the question, but the treatment of random variable's in SPJ et al's Composing contracts work may be of interest.

Beyond random variables themselves, it represents random processes as sequences of random variables which increase in size over time, reflecting the growth of uncertainty over time. This results in a tree of possible values which grows wider into the future. Small examples of these trees are provided in the papers. They're shown growing from left to right, with each column of values representing a random variable. Seeing random variables applied in this way may help explain them.

I wrote a small example implementation of this, here. The web interface for the examples generates the trees I mentioned.