New Year is Near

Guess the new year has an effect on me, one thing I should have done ages ago: going to quit smoking.

Operational Semantics Preserving Translations

Assume a lambda calculus (LCi) with side effects/impure function
calls: LCi = v | \v . LCi | (LCi LCi) | call LCi*. * is a sequence of terms.

An example term: (\x. \y. call (+) x y) 2 3. For convenience, I assume 2 and 3 are lambda encodings of the integers 2 and 3, similarly for +.

A call models an (impure/non-referentially transparent) system call. For simplicity, we assume that if two programs are run, and they have made identical calls, that any two new identical calls will return identical results.

I.e.: if two programs made (precisely) two calls to some function "tick" resulting in values 1 and 2, then the third call to tick will return the same value.

Assume the functions EAGER and LAZY, eager and lazy operational semantics for closed terms in LCi, respectively. They both map an LCi term into a value of type (LCi = call LCi*)* LCi, the collection of made calls in temporal order followed, possibly, by the term in strong normal form - fully reduced. I'll handwave termination concerns away for the time being. EAGER and LAZY are called the operational semantics since it tracks the system calls made and returns the evaluated term, if any. Note that I assume that a call only accepts an LCi term in strong normal form (fully reduced), and returns a term in strong normal form.

Examples:

EAGER((\x. \y. call (+) x y) 2 3) = (5 = call 2 3), 5.
During the evaluation of the term we made one call to +, returned 5,
and the whole program reduces to 5.

and

EAGER( (\x . call tick) (call tick) ) = (1 = call tick), (2 = call tick), 2.
Two calls to tick returned constants 1 and 2, the whole program reduces to 2.

moreover

LAZY ( ((\x. call (+) 2 3) (call tick) ) = (5 = call 2 3), 5.

whereas

EAGER ( ((\x. call (+) 2 3) (call tick) ) = (1 = call tick), (5 = call 2 3), 5.

Two terms are assumed to be operationally equal if they made exactly the same systems calls in temporal order, and possibly reduce to the same term, BUT two identical terms may return a similar result under the two impure operational semantics, but are not equal since they didn't make the same series of system calls.

Needed: two functions e_to_l and l_to_e such that EAGER(l) = LAZY(e_to_l l), LAZY(l) = EAGER(l_to_e l), EAGER(l) = EAGER(l_to_e(e_to_l l)), and LAZY(l) = LAZY(e_to_l (l_to_e l)). I.e., operational semantics preserving functions between eager and lazily evaluated impure LC terms where = is the alpha equivalence on series of terms.

Rationale: I want to implement some lazy features in Hi, this seems to be one good solution

Moreover:

1. Say you would like to implement a Haskell compiler but you only
have a Lisp compiler. Solution: translate Haskell to a corresponding
LCi term l, translate that term to l' = l_to_e l, translate l' to Lisp. Hereby solving the problem once and for all.

2. Say you want to have eager semantics in impure Haskell. That could be done similarly with the e_to_l function.

3. Conversely, you might want to translate Lisp to Haskell.

I didn't think it through too much, a simple CPS transform probably doesn't do it, but may be a good starting point.

Funny thing is that this is a totally opposing view to normal interpretations of operational semantics of LC since I am only interested in observational equivalence with respect to side effects. Which makes sense for someone who builds compilers since the only interesting quality of a program is what it does to the system and the result is often uninteresting.

(Unbelievably all my posts end up on the wrong blog.)

010610: There's an addendum to it. During rewriting, one of the properties I want is that whenever a call is rewritten, all arguments are constants, i.e. normalized.

Language Jokes

For professionals:

For lay men:

Log 12/20/09

After a number of changes, some small, some large, the to ml compiled compiler accepts its own system file again. It also cleanly compiles simple programs to C (fac, list manipulations). Various thoughts:

1. I simplified the type checker to a prover using solely antecedents and consequents. Both are stored in a list, giving quadratic behavior. It should become O(n x log(n)) here.
2. In order to avoid quadratic behavior I tried to avoid alpha conversion on lambda terms. There have been/are too many bugs because of that. Should solve this.
3. I don't inline yet. I should do this at some point.
   
4. The method invocations are compiled down to combinators. Case statements are a linear collection of tests, that means linear behavior on lookups. Not sure this is a problem actually.
5. Everything not essential graph rewriting is done through FFI (libffi) where all functions are loaded from dynamic libraries (libdl). Every FFI call is evaluated each time. FFI is slow already, I could/should add memoization here.
6. FFI calls are dynamic in nature leading to runtime failures when types are not matched. Should look into swig to automate the glue.
7. I should allow unary arguments to FFI, now it is assumed all FFI symbols refer to functions.
   
8. I wonder how combinators will work out long-time. There might be just too much copying - should think over how spurious copying can be avoided.
   
9. I need serialization. This should be simple and obvious if all data is treated as trees.
10. I started on a simple ReST parser for documentation which I intend to be part of the compiler.
11. I should prove the type system correct?

This ended up on the wrong blog something fishy on blogspot?

Indirection

David Wheeler once said:

All problems in computer science can be solved by another level of indirection ¹

And Kevlin Henney answered:

...except for the problem of too many layers of indirection. ²

¹ Diomidis Spinellis. Another level of indirection. In Andy Oram and Greg Wilson, editors, Beautiful Code: Leading Programmers Explain How They Think, chapter 17, pages 279–291. O’Reilly and Associates, Sebastopol, CA, 2007.
² http://en.wikipedia.org/wiki/Indirection_(programming)

Taken from http://www.omninerd.com/articles/Coding_Practices

Final Exit

Karen Stern’s Final Exit
October 29, 2007, Kingman, Arizona

By Richard N. Côté / dickcote at earthlink.net

Karen Stern, a vivacious 53-year-old,
guitar-playing singer and writer of loopy,
infectiously funny songs, died on the morning of
October 29, 2007, in a motel in Kingman, Arizona.

She had informed the front desk clerk about 7:00
a.m. that she would be checking out that day.
When she had not done so by 11:00 a.m., a motel
staff member went to her room.  Karen was found
in her bed, neatly dressed, with an empty tank of
helium gas nearby. She had committed suicide in a
gentle, painless way by breathing pure helium,
which rendered her unconscious within a minute or
two and dead within five or ten minutes. The
hotel immediately called 911, but the paramedics 
could do nothing to help her.

A native of the Northeast, she had chosen
Kingman, Arizona, as one of her temporary
sanctuaries in the last several years. Its dry
climate offered some relief from the severe
effects of the two baffling and exhausting
afflictions from which she had suffered for many
years: Morgellons Syndrome and Chronic Fatigue
and Immune Dysfunction Syndrome (CFIDS).

According to the CFIDS Association
(www.cfids.org), “Chronic fatigue and immune
dysfunction syndrome, also known as chronic
fatigue syndrome (CFS), myalgic encephalomyelitis
(ME) and by other names, is a complex and
debilitating chronic illness that affects the 
brain and multiple body systems.”

Morgellons Syndrome is equally baffling to
science. The Morgellons Research Foundation
(www.morgellons.org) found that although some
patients did find physicians willing to help
them, “many patients reported feeling abandoned
by physicians unwilling to investigate their
illness. These patients tried valiantly to find a
modicum of relief in the face of an otherwise
ineffective medical system.” Karen, who spent
years intensively researching her ailments,  
was one of those patients.

Numerous doctors could not alleviate the
increasingly tortured existence she had lived for
the past several years. As her conditions
worsened, and life became progressively more
unbearable, Karen consulted numerous experts on
the subject of suicide, and had received
extensive advice on how to find the strength to
live, as well as how to put an end to her pain
peacefully, should she choose to do so. She spent
an enormous amount of time conducting research on
how to achieve a rapid, painless death.

Ultimately, she chose the helium method because
it was recommended in the world’s best-selling
suicide how-to book, Final Exit, by Derek
Humphry, and because the supplies could all be
obtained locally, legally, and without having to 
involve anyone else.

17 x 17 is worth $298.00

There's a nice puzzle up on the Complexity blog. Can you four-color a 17x17 plane such that for all rectangles all corners have different colors?

Its easy to program actually, think I might give it a try.

The Alliance for Code Excellence

A world where software runs cleanly and correctly as it simplifies, enhances and enriches our day everyday life is achievable. Mitigating the scope and negative impact of bad code on our jobs, our lives and our world is our all–consuming passion.

Energizing the development world with the commitment and code excellence through code offsets is the key to our ultimate success and the realization of a sustainable code base that ushers in a new age of innovation that will propel humanity to a higher plane of existence.

"Its like, man, purple bunnies all the way." Guess its a good initiative, but they could have done without the higher planes.

48 Cores @ Intel

Costly because of big die-size even at 65nm; acclaimed low power consumption but heat sink doesn't fit into my hand bag.

Hypoglycemia

Darn, hypoglycemia, probably some brain damage -elevated glucose gives vasoconstriction/small vein damage,- due to serotonin syndrome due to untapered Effexor XR 75 mg/benzodiazepine after too much stress -a dead mum, a lady with PCOS,- faulty flight/fight response.

May not fit. Hmm, should test it.