Lambda the Ultimate

I have a question, which has arisen after running into an unexpected variable capture in a Python program I am working on.

Here is a sample:

def codeExample1(hashTable):
  def makeGenerator():
    for keyName in hashTable:
      def valueGenerator():
        for keyValue in hashTable[keyName]:
          yield keyValue

      yield (keyName,valueGenerator())

  return makeGenerator()

Now, I was expecting keyName in the function valueGenerator to be bound to the value of keyName at the current step in the iterator over hashTable, effectively creating a new copy of the valueGenerator function each step.

What occurred instead was that keyName was bound to the value of keyName at the last step of the iterator, effectively making each valueGenerator call the same.

To correct this unexpected behavior, one would rewrite valueGenerator to take a parameter like this:

def codeExample1(hashTable):
  def makeGenerator():
    for keyName in hashTable:
      def valueGenerator(_keyName):
        for keyValue in hashTable[_keyName]:
          yield keyValue

      yield (keyName,valueGenerator(keyName))

  return makeGenerator()

So that was a bit of a long lead in, but what I'm trying to get at is what is the name for the type of variable capture exhibited by Python in this example and what is the name of the variable capture I was expecting to occur?

Hi, I am doing some proofs on a calculus with existential types and I am fairly liberally applying Baredregt's convention (approximately that bound variables are distinctly named). My assumption is that I have to justify using this convention and that that justification is along the lines of 'the rules of the calculus abide by the convention'. However, I can not find any information about a formal way of justifying this. Does anyone have experience of this, or pointers to relavent papers?

Thanks, Nick

I'd like to tell a story. I'm an engineer working in the embedded world on compilers and simulators. Bored by the conservative approach to technology that I saw in companies, I started to learn Haskell/OCaml few years ago. It has been a valuable experience, especially for types.

Then, I tried to build a small product. I selected OCaml for practical reasons. I wrote a part of a binary translator. The reuse is great, and the code is amazingly short..

I then explained what I had done to my team. But during a discussion with my boss, I was told that "exotic languages are very similar to exotic holiday locations. You pay a premium to go there, but the only thing that is sure is that you will come back. Quite often, the only tangible trace of your stay is what you let in the hotel bin: an empty bottle of water and some papers. Please rewrite your stuff in C."

My conclusion is -- (1) I won't ever go on holiday with my boss and (2) I'm on the job market :)

Anybody who had a better experience?

If this question doesn't make sense, it's probably because I might be confused with the term subtype.

What is the correct mathematical symbol for subtype ?
if B is a subtype of A, which do I write:

1. B ≤ A
2. B <: A

Thanks.

Is co- and contravariance a concept related to inheritance or can it apply to normal method parameters ?
See definition at c2.com.

e.g. In java

    class Food{}
    class Grass extends Food {}
    class Antelope extends Food {}
    public class Main2
    {
        public static void main(String[] args) {
            Main2.eat( new Food() );
            Main2.eat( new Grass() );
            Main2.swallow( new Food() ); // compile-time error
            Main2.swallow( new Grass() );
        }
        public static void eat( Food f ) {}
        public static void swallow( Grass f ) {}
    }

So I get a compile-time error because the method parameters to swallow is covariant i.e. it only accepts Grass and its subtypes.

Am I correct in my reasoning ? Thanks

I wonder why I haven't heard more about Prop.

It lets you do ML-style pattern matching in C++. Perhaps a nifty way to sneak in a little functional programming at work.

Cyclic Proofs for First-Order Logic with Inductive Definitions, James Brotherston, in Proceedings of TABLEAUX 2005

We consider a cyclic approach to inductive reasoning in the setting
of first-order logic with inductive definitions. We present a proof
system for this language in which proofs are represented as finite,
locally sound derivation trees with a "repeat function"
identifying cyclic proof sections. Soundness is guaranteed by a
well-foundedness condition formulated globally in terms of
\emph{traces} over the proof tree, following an idea due to Sprenger
and Dam. However, in contrast to their work, our proof system does
not require an extension of logical syntax by ordinal variables.

This technique of making potentially cyclic proof-graphs is really nice since it makes the connection between recursive definitions in a functional programming language and a proof structure very obvious. There is no need to specify the inductive principle ahead of time, you can simply structure the proof tree as you would your functional code.

I've seen Fortress come upon the main page a few times, so I thought some people might be interested in a Fortress presentation by Guy Steele.

I imagine there is nothing new for people following the language, but for those, like myself, who don't, it makes for a nice overview. For instance, it explains how they are doing entry of that crazy mathematical notation.

I also found the explicit juxtaposition operator fascinating, though most likely I just haven't run across it's previous incarnations before.

I want to start making a compiler for a little programming language that I have in mind. I think that doing it right would teach me lot of new things. I want to target the JVM's bytecode using Jasmin or Jamaica but I want to know your opinions...

Is there another good choice to generate bytecode from the opcodes for the JVM?

What about other VM's? CLR is not as portable as JVM... I used Parrot once but i didnt like it in that time. Do you know other options?

Abstract: Array theory combines APL with set theory, transfinite arithmetic, and operationally transformed functions to produce an axiomatic theory in which the theorems hold for all arrays having any finite number of axes of arbitrary countable ordinal lengths. The items of an array are again arrays. The treatment of ordinal numbers and letters is similar to Quine's treatment of individuals in set theory. The theory is developed first as a theory of lists. This paper relates the theory to the eight axioms of Zermelo-Fraenkel set theory, describes the structure of arrays, interprets empty arrays in terms of vector spaces, presents a system of axioms for certain properties of operations related to the APL function of reshaping, deduces a few hundred theorems and corollaries, develops an algebra for determining the behavior of operations applied to empty arrays, begins the axiomatic development of a replacement operator, and provides an informal account of unions. Cartesian products, Cartesian arrays, and outer, positional, separation, and reduction transforms.

Preamble: The intention of the work reported here is to develop a theory of arrays, in terms of standard set theory, that will provide rigorous definitions for programming operations and thereby a logical foundation for the construction of programming languages. The present contribution is a first approach to establishing a comprehensive theory of arrays, and it is anticipated that future papers will extend and refine the concepts presented.

The objects used in programming are represented in a mathematical system of ordered collections as arrays of arrays. Simple axioms define certain primitive operations on the arrays. Most data operations in programming can then be represented by operations built upon the axioms. One of the starting points for the development of the theory is APL. Programs written in APL are used to generate corollaries of the axioms and to check the consistency of the system.

Although the paper was written for the specialist in mathematical logic, it should be of interest to the computer scientist and particularly to one who specializes in programming languages. Its chief contribution is an axiomatic theory for data structures, which includes explicit rules for transforming any operation into a new operation that applies to all items in any array.