Lambda the Ultimate

Hi,
I'm studying the lambda calculus and there's something I can't understand in the fixed point theorem.

I'm reading the Barendregt book Lamba Calculi with Types, but at the moment I'm studyng the untyped one, in the first part of the book.

It says there is a fixed point combinator: ( \ = lambda )

Y = \f.(\x.f(xx))(\x.f(xx))

such that

for any F, F(YF) = YF

So, if my F is just a variable, let's say F = q, then how

q(Yq) can become Yq?

I am sure I am missing something.
Can you help me?

Thanks,
Carlo

This is something I have been wondering about recently..

The basic idea is memoized data that decays over time.

• The first time data is required it is calculated
• If it took substantial time to calculate it is memoized and calculation time recorded
• Subsequent requests to the data (with same parameters) are given the memoized version
• The memoized data decays over time based on a metric that incorporates data size, calculation time, last access time, current memory load and so forth
• Once the memoized data has fully decayed, it is freed from memory
• Future requests to the data cause it to be recalculated, and (re)memoized
• Repeat

At first glance, this seems like it might give a nice dynamic time/space balance to certain aspects of a programming language.

Having not come across the idea before, I was wondering if anyone might point me towards any languages or papers on the subject?

FringeDC is a group interested in exploring fringe languages, such as Lisp, Haskell, Prolog, ML, etc.

Presentation Title: "Emacs as a Development and Deployment Paradigm" by Philip Fominykh

(Also, Jame Webb and Conrad Barski will discuss the EMACS port of "Casting SPELs in Lisp", a Lisp tutorial/comic book.)

meeting location/details: http://www.lisperati.com/sept22.html
main site: www.lisperati.com/fringedc.html

I have a question. Isn't it more useful to bring uniqueness type to languages like C# and JAVA, instead of implementing STM in VMs?
STM has more impact on what developers and compiler is doing by now. But most of the code we are developing by now are not concurrent by default. So if the current type systems force "uniqueness type" for all imperative-types in C# or Java, most of our programs that are already developed, should work.
On the other hand concurrent programming model will not change current developing methods very much, and syntax remains almost untouched.
(Of course I prefer a expression-based, declarative language. But that would not happen without a Microsoft or Sun behind it! :) )

&Hello Folks,

I am a CS student on my first year. I've been reading LtU for some years already and obviously most of the topics here are way beyond my current knowledge. This is my first post detailing something I did which I am kinda proud of.

At my university we have a chair called "computer architecture;, in this class they teach us some assembly language for a non-existant x86 machine. We use the SIMx86 simulator for our exercises. In this university we have two examinations per chair and one extra final examination in case you failed passing with the previous two. The second examination was composed only of assembly language questions.

My problem was that I skipped (yes, true) the assembly language classes trusting I could learn it later but when I went to study, I discovered that SIMx86 would only run on windows machines and I have a mac.

It was the night before the examination and I decided on a bold course of action, I decided to code my own assembler interpreter, an ad hoc solution, just good enough to run the exercises we learned. In about five hours, I ended with this design:

Cute X86 GUI

I've called it CuteX86 and implemented only the subset of assembly I needed for my exercises. I've added a debugger that allowed me to run my source step by step inspecting the "memory".

It is not a solution or a product, it is just a tool that I built to aid myself studying. I've created it using Runtime Revolution language which is a "successor" of old Apple HyperCard.

The implementation is really easy, the code is stored in memory as a string and is executed line by line, instead of parsing the whole source and doing a real job, I analyze each executing line converting it to the appropriate Runtime Revolution code to be executed in runtime. This code calls a big switch statement where all the instructions are implemented. There are four register and minimal memory access. I know this is not the proper way of building interpreters but this was not a general purpose tool, it was a way for me to learn assembly so I could pass the examination and not waste my tuition.

I've finished it 2:00 AM and studied till 7:00 AM, took the examination at 8:00 AM and actually passed the thing! (thats why I am happy). By building my own interpreter, I had a deeper knowledge of what was actually happening than my peers, in the end, I could do the examination just by thinking how my code would process something.

Now I am sharing this interpreter with the other students, and even integrated a simple "source code hosting" portal into it so that we can share code.

I always loved computer languages, just bought myself the dragon book, SICP and The Art of Computer Programming Vol 1. Someday I may just be able to write real languages :-)

PS: I am specially proud of my jumping routines!

Andre

The n-category café give the links to an interesting series of online courses about category-theorical monads and their link to algebras. I found them clear, precise and very helpful, even if they are generally more oriented towards mathematicians than computer scientists.

• Monads 1: Definition of monad. Some examples.
• Monads 2: Examples continuation. The monad for categories
• Monads 3: Algebras for monads
• Monads 3a: Answers to some questions
• Monads 4: The category of algebras of a monad

Blackboards rules ! :)

I am interested in constructing higher-order functions (e.g. map/filter/fold) from stack-based byte-code generated from non-functional languages (like Java), where most things are expressed in for-loops. I am wondering what keywords would lead me to related work and if anyone knows some good papers to start with?

Hi,

I'm trying to understand the stutter invariance and its application in the verification distributed systems (specified in the the SPIN model checker, primer and reference manual).

I couldn't quite understand the concept. Could anyone help me to understand it ?

Thanks in advance,
Mohan...

I wonder whether the following extension to the type inference mechanisms of languages like Haskell, ML, etc. would be possible, and, if so, desirable.

Today we write functions like

head (a:_) = a

and get warning messages concerning patterns not covering all possibilities. This is fine. However, I am not being warned when the compiler sees code like

head []

(even when head were defined like above, without a default clause that raises a runtime error.)

In principle, though, the type inference could collect for each value of algebraic datatype by which constructor this value could possibly have been created.

For example, the type of
unJust (Just x) = x
would not be (Maybe a -> a), but something like
(Maybe{Just} a) -> a
Consequently, the type of Nothing would be (Maybe{Nothing} a) and the type checker could flag occurences of
unJust x where (x::Maybe{Nothing} a)
or
head y where (y::[a]{[]})
as type error.

The consequence would be that it would be no longer worth a warning when writing functions with incomplete patterns. Rather, at the place where the function is used the compiler would be able to diagnose one of three outcomes:
- this will fail (when the intersection of the constructor sets is empty)
- it may succeed (when the intersection is not empty)
- it will succeed as far as pattern matching is concerned (when the constructor set of the type of the argument is a subset of the constructor set of the function argument type)

Case 1 could be treated like just another type error. Case 2 could provoke a warning. Case 3 is ok, of course.

To be sure, that would also encourage a different style. Instead of writing dozens of meanigless default cases like
foo _ = error "can't happen"
one could leave that out and let the compiler prove that indeed it can't happen.

(I hope I could express my thoughts clear enough despite english not being my native language.)

A really dump question...

The associativity law states (using Haskell syntax):

m >>= (\x -> k x >>= h) = (m >>= k) >>= h

What I don't understand is why "bind" can be associative. One use of monad is to encapsulate side-effects. And the order of operations is important when there are side-effects. If so, why does associativity hold?