Lambda the Ultimate

Functions are sometimes defined in terms of sets as the binary relation that relates each x to (f x), but this seems fundamentally wrong to me, because sets bear an immediate resemblance to lambda expressions.

1. Lambda abstractions are similar to set comprehensions. Compare {x | M} to (λ x . M) (or {x:A | M} to (λ x:A . M)).
2. Application syntax is identical to predication syntax. Compare (f x) to (f x). (If by (f x) we mean (x ∈ f) or, using prefix, (∋ f x), then ∋ corresponds to the application special operator sometimes written as @.) Note that ∋ and @ are special operators (to use Lisp terminology) not functions or relations. It is sometimes claimed that ∋ is a relation on sets but that cannot be the case because if you define relations using set membership then (∋ x y) means (∋ ∋ ⟨x y⟩), i.e. (∋ ∋ ⟨∋ ⟨x y⟩⟩), ad infinitum, which does not make sense. Rather, ∋ and @ are primitive concepts (special operators).
3. The beta reduction rule holds for both systems. Compare ((λ x . M) N) →_β (subst x M N) to (∋ {x | M} N) →_β (subst x M N).
4. The eta reduction rule holds for both systems. Compare (λ x . (M x)) →_η M to {x | (∋ M x)} →_η M (for x not free in M).

Etc. So I think the proper way to do things is to equate sets and predicates and to define a set as a function that returns a Boolean. I thought I had come up with this but it turns out Church had thought the same thing (calling this function the characteristic function IIRC) and it is also called the indicator function.

Given all this, can somebody tell me why mathematicians keep making a distinction between sets, predicates and their indicator functions (other than historcial reasons)? Why not simply equate sets, predicates and their characteristic functions?

Hello,

I'm proposing a Programming Language Theory WikiProject on the English-language Wikipedia. A WikiProject, for those unfamiliar, is a group of Wikipedia editors who write and edit articles (for the Wikipedia) on specific topics, ensuring consistent quality, formatting, and such.

Note that this is not:

* A WikiSpaces project;
* Competition for, or redundant with, the proposed LTU wiki

Instead, it is a project to improve Wikipedia's coverage of these topics, which is currently spotty. The output of the project will be encyclopedia articles (new or improvements to existing articles) on subjects related to PLT theory.

As such, Wikipedia guidelines will need to be followed; the main ones which apply are:

* Verifiablity--any and all claims must be supported (or at least supportable) by references to the appropriate literature.
* NPOV--all significant sides of controversial issues need to be reflected--and again, attributed to sources outside of Wikipedia. (This does not mean we have to include the opionions of trolls and such--significant means significant). Statements and claims which are opinion or speculation are generally unwelcome, unless they can be externally sourced.
* No original research. This is not the place to discuss original ideas, publish research, or hold discussions on new or novel ideas. Nor is Wikipedia a discussion forum (though discussion relevant to the articles is welcome in the talk pages).

The focus is writing articles for an encyclopedia. (This is why this is not at all a replacement or competition for LtU, or the proposed LTU wiki).

One former Wikipedia policy which used to be in force, but has largely gone by the wayside, is the avoidance of specialist articles and subjects. Wikipedia currently hosts articles--understandable only by specialists in the field--on many topics, such as physics. Original research--as stated above--is out, but technical subjects well-supported in the primarly literature are welcome.

If you're interested, follow the link above (which points to a subpage of my homepage; I'm EngineerScotty on WP) and comment! If don't currently have a WP membership, creating an account is free and easy--the link to do so is at the top of every page on Wikipedia.

Thanks!

Stanford University, Oct 24, 2005

The nice thing about a language that takes hold is that you can work with it again and again. In 30 years we have built Smalltalk systems with quite different constraints. This talk will examine a few of these, and show how tricks of the trade can be applied to enhance one aspect or another and, frequently, to make real progress.

The topic "Choice of OS of LtU readers" asked the wrong question and hence got a sequence of boring I use Linux or I use Windows answers. So let's ask the Right Question.

What new OS shows most promise of ...
a) Doing "The Right Thing" (in the Programming Language Designers overwhelmingly over developed Sense of Right),
b) Being usable in the near term,
and, as such, merits our attention, support and dual boot disk space?

A quick bit of Googling and weeding of the results turns up...

• Brix - Everything must be compiled to a "safe" meta language called Tetra

• Inferno (A Plan 9 derivative with "safe" language Limbo.)
• Plan 9 - Everythings a file, and a file is just a stream of bytes, and who cares where network wise where any thing really is.
• Unununium

Any other suggestions / commentary on these OS's most welcome.

Instead of emphasizing the what, I want to emphasize the how part: how we feel while programming. That's Ruby's main difference from other language designs. I emphasize the feeling, in particular, how I feel using Ruby. I didn't work hard to make Ruby perfect for everyone, because you feel differently from me. No language can be perfect for everyone. I tried to make Ruby perfect for me, but maybe it's not perfect for you. The perfect language for Guido van Rossum is probably Python. -Matz.

Has anybody, then, made systems which might some day convert any language into any other language in a clean fashion, so that I can write in Alice ML and you can modify it in Java? Personally, I think it is obvious that even if such transmogrification were avaialble, it wouldn't always help a heck of a lot because the density of any given region of code can change like 100x. Not to mention that I guess any Turing-esque equivalency doesn't take into consideration the differences in runtime.

Another take on this: Why aren't there programming language generators / wizards which ask me a series of 20 questions ("do you prefer static or dynamic typing?" - i'd like to be able to answer 'both', of course) and then spit out a framework language (including debugger!) for me? (And under the covers everything gets converted to/from XML so we can individually put the curly braces - if any - wherever we prefer.)

Here you can find some amazing(!) peer reviews of a few famous papers (by Dijkstra, Turing, etc.).

The Jekyll Programming Language:

Jekyll is a high level programming language that can be translated
both to and from human readable, human editable C. Not only can the
C version of a file be generated from the Jekyll version, but the
Jekyll version can be generated from the C version. By being inter-
convertible with C, Jekyll removes the need for companies to take the
risk of moving their projects to a new language. A program can be ported
to Jekyll one file at a time, or one programmer at a time. If the Jekyll
compiler ceases to be available, or a tool doesn’t support Jekyll, or a
programmer doesn’t understand Jekyll, this is not a problem as one can
just use the C code. Jekyll enhances C with many high level features,
including safety, generic types, stack allocated lambda expressions,
and type classes. All features have been carefully designed so that they
map elegantly to and from C.

It allows statically resolved generics as well as dynamic dispatch. Too
bad about the C-like syntax ;-)

A totally different question for in the fun department,

I was wondering about the 'geekiness' of the LtU crowd. As one of the measures of that would be choice of OS people work on, I wondered

What is your favourite OS you work on (at home, or at the office)?

I run Fedore Core 3 on an Asus S5N notebook.

I just started reading "Type Theory and Functional Programming" and realised pretty rapidly that I wasn't sure what a proposition was.

When I look at Wikipedia - http://en.wikipedia.org/wiki/Proposition - they seemed rather negative on the whole idea. If propositions are questionable how can you do something as concrete as write programs with them?

Am I just getting two different meanings of "proposition" mixed up? In the article it says

In Aristotelian logic a proposition is a particular kind of sentence: one which affirms or denies a predicate of a subject.

Even I know what a predicate is, so should I just run with this definition?

Thanks.

More shameless self-promotion from me: here's a paper I've been working on that may be of interest to LtU readers, "Many cyclic block diagrams do not need parallel semantics."

It is about parallel vs. sequential semantics as applied to an interesting block diagram. (Here the adjectives "parallel" and "sequential" are used as they are in discussions of the full abstraction problem rather than in discussions of concurrency.) It also introduces a block diagram extension to Haskell I've been working on.