## User login## Navigation |
## archives## Proposed Wikipedia Programming Language Theory topicHello, 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 * A WikiSpaces project; 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. The focus is writing articles for an encyclopedia. (This is why this is 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! ## Lambda the Ultimate Set ComprehensionFunctions 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. - Lambda abstractions are similar to set comprehensions. Compare {x | M} to (λ x . M) (or {x:A | M} to (λ x:A . M)).
- 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). - The beta reduction rule holds for both systems. Compare ((λ x . M) N) →
_{β}(subst x M N) to (∋ {x | M} N) →_{β}(subst x M N). - 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? |
## Browse archives## Active forum topics |

## Recent comments

6 hours 55 min ago

7 hours 8 min ago

3 days 19 hours ago

4 days 9 hours ago

4 days 12 hours ago

6 days 10 hours ago

6 days 12 hours ago

6 days 13 hours ago

6 days 20 hours ago

1 week 27 min ago