Re: To observe is to......EC

From: Bruno Marchal <>
Date: Mon, 13 Nov 2006 12:37:38 +0100

Le 12-nov.-06, à 03:43, Colin Geoffrey Hales a écrit :
> As I stuff my head with the bird menagerie, and try to see if I need to
> breed a new bird, I find that EC is best thought of as a form of
> combinatorics (as you thought, Bruno!).
You should use "combinators" instead of "combinatorics" because most
people will confuse those two very different branches of math.
Combinators are just sort of lambda terms without variable.
> Is there anyone out there who has any intuitions as to which bird(s)
> would
> correspond to 'coherence' or 'symmetry breaking'?
All eliminators, like the kestrel, introduce some irreversibility in
the computations.
Duplicators, like the warbler, can break symmetry in their own ways.
> I find that I must have
> some sort of 'adjacency' or 'proximity' applicator. Perhaps, with the
> bird
> metaphor, I need birds that have selective hearing and hear better
> those
> birds that are closer, where 'closer' means 'I can hear you'.
Ah ah! I guess you need to type your lambda terms (or the combinators).
Then you will be able to benefit from the very extraordinary relation
between lambda terms and proofs known as the Curry Howard isomorphism.
This is in fashion today and you will find many interesting papers
about this on the net. The Curry Howard iso provides also a relation
between "weak logic" and computations.
BTW there are more and more genuine "quantum lambda calculus", but from
the point of view of extracting physics from computations this can be
seen as a form of treachery.
The most typical models for lambda are "cartesian closed category".
Actually "lambda calculus" provides a deep computer science motivation
for the whole of category theory, but this is a bit "advanced logic"
perhaps. There are good books by Lambek, Asperti & Longo, etc.
> Also... is there a 'Nothing' or a 'Vanishing' bird? If a 'normal form'
> completely dissappears to 'Nothing', then its normal form is 'Nothing'.
> Trying to axiomatise 'Nothing' seems a tad tricky, but I'm getting an
> idea
> of what it might be. Kestrelling to a Konstant 'nothing' seems useful
> but
> I'm not sure how to formalise it or whether that is the right way to
> think
> of it. The confusing difference is between 'doing nothing' and 'being
> nothing'.
There are programming languages which allow the "empty program", but to
my knowledge this does not make sense in lambda or combinators. I will
think about this ...
> I can't believe what I just wrote, but they are serious questions from
> a
> newbie combinatoricist. Patience is required.
Sure. Wish you luck.
> Funny how these things work out. I know it sounds a little obtuse, but
> I'm
> going to leave it there for now. If anyone wants a nice 'programmers
> intro' to Lambda Calc: Michaelson G. 1989. An introduction to
> functional
> programming through Lambda calculus.
> Nice bird intro here:
That is good indeed (but not quite standard).
There is also the Smullyan pocket book: "How to Mock a Mockingbird?".
The birdy names of the combinators comes from it.
And then the best (because the only one :) intro to combinators on the
A summary and a follow up of those post can be found in my last
(Elsevier) paper which I should put on my webpage or send to
(Please, ask me personally a copy if you want a free print quickly).
The best textbook on (untyped) lambda calculus remains, imo, the book
by Barendregt (North Holland).
(If you read it, and if you are not mathematician, please jump over the
first chapter which is very difficult and not useful for the
 You received this message because you are subscribed to the Google Groups "Everything List" group.
To post to this group, send email to
To unsubscribe from this group, send email to
For more options, visit this group at
Received on Mon Nov 13 2006 - 06:38:07 PST

This archive was generated by hypermail 2.3.0 : Fri Feb 16 2018 - 13:20:12 PST