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.


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.


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.


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


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


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?



    David Wheeler once said:
    All problems in computer science can be solved by another level of indirection 1
    And Kevlin Henney answered:
    ...except for the problem of too many layers of indirection. 2

    1 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.
    2 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.



    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.