Lambda the Ultimate

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!

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?