Lambda the Ultimate

I've read this site for some time, but now I have a question I believe the people at LtU could answer. The question is what are some of the current applications of formal semantics.

I've read or skimmed through some semantics textbooks, like Winskel's, and some less well-known, but a question they rarely answer in a satisfactory manner, at least to me, is why I should try to model the semantics of a language formally in the first place. Usually, the books say in the very beginning that semantics is useful for verification and program analysis, and then say no more about it. That's the reason I tried to get hold of a copy of Semantics with Applications as soon as I discovered it (an old edition is available online). The applications mentioned in the book are proving the correctness of an implementation, program analysis, and axiomatic program verification.

I've also seen recently the papers about expressing semantics in theorem provers, like here. It's cool that it is possible to extract an interpreter and a module for program analysis from the proofs about semantics. But we could just code the interpreter and program analysis; yes, I know, extracting them from a prover makes them more trustworthy. I refrain from saying that they are "correct" because it would depend on the correctness of the theorem prover, the compiler for the language, the extraction process, etc. Also, I don't know how this idea would fare in bigger, more realistic languages.

So, although I have seen already some applications of formal semantics, nothing of it quite managed to impress me much. What is it, then, that we gain by modeling the semantics of a language formally? What we can accomplish with a semantics that we couldn't without? What would be possible without a formal semantics, but difficult and/or clumsy? What examples do we have of sucessful and important applications of formal semantics to programming practice?

I think this is very much worth knowing, the questions are worth asking, and the books don't provide answers. So maybe LtU can :)

I'd think I want to allow a function with this type:

proc(class T cls) : T

And I want such functions to support type subclasses. For a simple instantiating example:

proc myfun(class Employee empcls) : Employee
return empcls.new()
...
Manager m = myfun(Manager);

Where

class Manager(Employee)
bonus : Dbl = 2.5 * salary; // :-)

Is this "principle of least surprise"? commonplace? or are there gotchas I'm not thinking about.

Thanks much.

Scott

I was putting together a small typechecker with a friend, who argued that the most straightforward way to determine the types of members of a set of mutually recursive functions would be to initially set the types of all to _|_, then up to a fixed point update the var/type environment with what's known about the return type of each function. After that process, if any type association contains _|_ then the type check should fail.

That definition would have rejected something like let rec f x = f x, which in O'Caml has type forall A . forall B . A -> B.

So my question is, are there important functions that my friend's definition leaves out? I know that "Types and Programming Languages" would have us apply fix at the term level, but where can we go with this approach?

Okay, this might seem like an odd question, but is there contention on whether or not a while loop that performs assignment on local function variables is pure functional? For example the following Java code:

int process(int[] xs) 
{
  int zeros = 0;
  int sum = 0;
  int i=0;
  while (i < xs.Size) {
    if (xs[i] == 0)
      zeros++;
    sum += xs[i];
    ++i;
  }
  return sum - zeros;
}

Now I have heard frequently that the above code is considered to have side-effects because of the local assignments to variables. However, the mapping to pure-functional stack-based code (here shown in Cat) is very straightforward:

define process {
  // top argument = xs
  0 // zeros
  0 // sum
  0 // i
  [
    dig3 // bring xs to top of local stack
    dupd swap get_at eqz // xs[i] == 0
      [[inc] dip3] // inc zeros
      []
    if
    dupd swap get_at // tmp = xs[i]
    [bury3] dip // put xs to bottom of local stack
    swap [add_int] dip // sum += tmp
    inc // ++i
  ]
  [
    dig3 count [bury3] dip // tmp = xs.Size
    dupd lt_int // i < tmp
  ]
  while
  pop // remove i
  swap sub_int // sum-zeros
}

So, my problem is that I am not sure whether this is old news or new news. Any feedback would be appreciated.

Over at Russ Cox's blog:

In 1997, on his retirement from Bell Labs, Doug McIlroy gave a fascinating talk about the “History of Computing at Bell Labs” ...

My favorite parts of the talk are the description of the bi-quinary decimal relay calculator and the description of a team that spent over a year tracking down a race condition bug in a missile detector (reliability was king: today you'd just stamp “cannot reproduce” and send the report back). But the whole thing contains many fantastic stories. It's well worth the read or listen. I also like his recollection of programming using cards: “It's the kind of thing you can be nostalgic about, but it wasn't actually fun.”

I was playing around with defining grammar productions rules for shapes in a 2d grid. Seems like using this type of scheme to generate complex shapes is very easy. But going the opposite direction and recognizing the language is impossible. If one has a grid consisting of cells filled with all terminal characters, if an arbitrary cell is chosen and the attempt is made to derive a parse tree from this cell, the ambiguity mounts quickly. Basically, any cell picked will give a different parse tree.

Thinking about it, this approach should generalize to grammars applied to graphs. Googling about for a bit and viewing the bibliograph statistics shows that there was some work done in this area in the late 90's but has since entirely disappeared:

Bibligraph stats for "graph grammar"

So, is anyone familiar with this area? Why did work in this area (almost) completely stop? Looks like some work was oriented toward parsing visual programming languages...

Is there any work proposing a minimal set of orthogonal operators to make an APL like language?

APL, J, et. al seem to mix what in other languages most people (or at least I) would call core language vs. library functions. I'm interested in the core language. In particular, it's not clear to me which are the adverbs required to operate on different kinds of array slices.

If, for example, I have three functions (X a), (Y b), (Z c); and suppose that each has been complied and proven correct somehow. Now if I compose the three functions (X (Y (Z c))) is the answer proven also given the types match. I remember a paper posted on the home page that seemed to prove this, but can't seem to find it.

After reading about like and wrap in Ecmascript I began thinking about possibility of at compile time checking that parameters passed to functions are a duck for that method. For example say you had:

def quack(duck):
duck.aMethod()
duck.anotherMethod()


It would see that duck requires aMethod and anotherMethod methods, and then check that all calls to quack pass in types that have these methods. Is something like this possible? Or am I failing to see something important that prevents having static analysis for duck typing languages.

Commutativity of operations and functions can be a useful thing for a compiler to know. So how do you you tell the compiler an operator or function is commutative (or associative, etc.)? One obvious option would be to let programmers tag their functions. This is bound to introduce subtle and nasty errors in to the code if the programmer makes a mistake. Not to mention it is inelegant, and it isn’t the kind of thing I want to see mixed in people's code (optimization hints that is).

So the big question is, how do we automatically recognize proprerties of functions like commutativity? In Cat (like Haskell) there is already a system for expressing rewriting rules (e.g. rule { $a $b f } => { $b $a f }). This fairly obviously demonstrates the commutativity of 'f'. In fact if we can follow any sequence of rewriting rules to arrive at this equality (which is a simple graph search problem), then we can also deduce commutativity.

I am trying to track down related research on the subject. If anyone has any pointers, I would be most appreciative.