Tag Archives: extensionality

Past vitalism in extreme functional programming

In Vitalism everything is a function.  Just like in lambda calculus with eta reduction.

opium

With chemlambda we are someplace corresponding to The Sceptycal Chymist: or Chymico-Physical Doubts and Paradoxes, by Boyle.

Recall that chemlambda (and GLC) rejects extensionality, because it is a global move, not a local one.

Therefore, chemlambda and GLC are not functional, properly speaking. Which is good, actually, for a variety of reasons, kind of the same as the ones why chemistry is better than vitalism.

In another post, this way of seeing was called “extreme functional programming“.

I hope this might help the understanding of distributed GLC model of computation and the reasons behind choices which were made in the model.

___________________________________

Notes:

1. Criticism of vitalism  supports the view that functional programming with extensionality is an reenactment of vitalism.

Vitalism has sometimes been criticized as begging the question by inventing a name. Molière had famously parodied this fallacy in Le Malade imaginaire, where a quack “answers” the question of “Why does opium cause sleep?” with “Because of its soporific power.”[29] Thomas Henry Huxley compared vitalism to stating that water is the way it is because of its “aquosity”.[30] His grandson Julian Huxley in 1926 compared “vital force” or élan vital to explaining a railroad locomotive’s operation by its élan locomotif (“locomotive force”). [quote from the wiki source on vitalism]

2. From the wiki source:

The Sceptical Chymist: or Chymico-Physical Doubts & Paradoxes is the title of Robert Boyle‘s masterpiece of scientific literature, published in London in 1661. In the form of a dialogue, the Sceptical Chymist presented Boyle’s hypothesis that matter consisted of atoms and clusters of atoms in motion and that every phenomenon was the result of collisions of particles in motion. For these reasons Robert Boyle has been called the founder of modern chemistry by J. R. Partington.[1]

 

3. Chemlamba is based on a chemical metaphor. The initial name of the formalism is “chemical concrete machine”, in contrast with the “chemical abstract machine” of Berry and Boudol.

___________________________________

 

No extensionality, no semantics

Extensionality, seen as eta reduction, or eta conversion, is a move which can be described in GLC, but it is global, not local.

See this post for the description of the move. The move is called “ext1”. I borrow from that post the description of the move.

Move ext1.  If there is no oriented path from “2″ to “1″ outside the left hand side picture then one may replace this picture by an arrow. Conversely, if there is no oriented path connecting “2″ with “1″ then one may replace the arrow with the graph from the left hand side of the following picture:

ext1r

Why is this move global? Because of the condition “there is no oriented path from “2″ to “1″ outside the left hand side picture”.  This condition involves an unbounded number of nodes and arrows, therefore it is global.

Further I shall make the usual comments:

  • the move ext1, by itself,  can be applied to any GLC graph, not only to those graphs which represent lambda terms. In this respect the move ext1 is treated like the graphic beta move, which, in GLC, can be applied to any graph (for example to graphs which are used to encode knot diagrams, or other examples of graphs which are outside the lambda calculus sector of GLC, but nevertheless are interesting),
  • if we restrict the move ext1 to lambda graphs then we have another problem: the condition “is a lambda graph” is global.

That is why the move ext1 is not considered to be part of GLC, nor will be used in distributed GLC.

You may remark that   GLOBAL FAN-OUT is a global move, which is part of GLC.  The answer to the implicit question is that chemlambda, which is a purely local graph rewriting system, solves this. Even if chemlambda and GLC are different formalisms, when it comes to universality, then they behave the same on lambda graphs, with the bonus on the chemlambda side of being able to prove that we can replace the use of the GLOBAL FAN-OUT with a succession of moves from chemlambda.

This can’t be done for the move ext1.

And this is actually good, because it opens a very intriguing research path: how far can we go by using only locality?

That means in particular: how far can we go without semantics?

Because:

  • extensionality brings functions
  • functions bring types
  • types bring the type police
  • the type police brings semantics.

It looks that life (basic works of real lifeforms) goes very well:

  • without semantics
  • with self-duplication instead of GLOBAL FAN-OUT (or even instead recursion).

In this respects distributed GLC is even more life-like than it looks at first sight.

Extensionality in graphic lambda calculus

This is part of the Tutorial:Graphic lambda calculus.

I want to discuss here the introduction of extensionality in the graphic lambda calculus. In some sense, extensionality is already present in the emergent algebra moves. Have you noticed the move “ext2”?

However, the eta-reduction from untyped lambda calculus needs a new move. I called it the ext1 move in arXiv:1207.0332 [cs.LO] paragraph 2.7. It is a global move, because in order to use it one has to check a global condition (without bound on the number of nodes and edges involved in the condition). In the mentioned paper I stated that the move applies only to graphs  which represent lambda calculus terms, but now I see no reason why it has to be confined to this sector, therefore here I shall formulate the ext1 move in more generality.

Move ext1.  If there is no oriented path from “2” to “1” outside the left hand side picture then one may replace this picture by an edge. Conversely, if there is no oriented path connecting “2” with “1” then one may replace the edge with the graph from the left hand side of the following picture:

ext1r

This move acts like eta-reduction when translated back from graphs to lambda calculus terms. “Ext” comes from “extensionality”.

Let us see why we need to formulate the move like this. Suppose that we eliminate the global condition  “there is no oriented path from “2” to “1” outside the left hand side  of the previous picture”. In particular let us suppose that there is an edge from “2” to “1” which completes the graphs from the LHS of the previous picture. For this graph, which appears at left in the next figure, we may use the graphic beta move like this (numbers in red indicate how we use the graphic beta move):

non_ext1_move

If we could apply the ext 1 move to this graph, then the result would be the following:

non_ext1_move2

Not only the result of this move is one loop, but it is the “wrong” loop, in the sense that this loop is obtained by closing the edge which vanishes in thin air when the graphic beta move is applied. There is no contradiction though, unless we wish to decorate the edges (i.e. to evaluate the result of the computation). It is just strange.

There is one question left: why the move called “ext2”, which is one of the emergent algebra moves, is also an extensionality move? A superficial answer is that the move ext2 says that the dilation of coefficient “1” is the identity function.

_____________________________

Return to Tutorial:Graphic lambda calculus