A question and a comment about untyped lambda calculus

Question: Is there any formulation in terms of category theory of pure untyped lambda calculus, only with alpha-equivalence and beta-reduction, but not with eta-reduction? Please provide links to the relevant sources, which have to contain proofs.

My impression (which could be wrong) is that the answer is NO. It becomes YES with eta-reduction, am I right?

Comment: This is again about pure untyped lambda calculus, only with alpha-equivalence and beta-reduction. compared with my graphic lambda calculus.  So, in pure untyped lambda calculus there are only two moves: beta-reduction and (a collection of moves under the) alpha-equivalence. At first view, the graphic lambda calculus has much more moves. Let us neglect the emergent algebra moves, which are exterior to lambda calculus. Still, in graphic lambda calculus there are the  fan-out moves    and the pruning moves. Compare these moves with the long prose one has to write in order to really explain how alpha-equivalence works and how terms are written, with all rules and moves included so that a non-human computer might apply them.

UPDATE: The question, formulated as: “is lambda-beta representable?” is an open problem by Barendregt and others. See for the precise language the paper GRaph models of lambda-calculus at work, by C. Berline, Math Struct. for Comput. Sci. 16:1-37, 2006,  link to ps.

Advertisements

Dual of the graphic beta move implies some Reidemeister moves

For the extended beta move see the dedicated tag.  See also the tutorial “Introduction to graphic lambda calculus“.

The extended beta move is still in beta version. In this post I want to explore some consequences of the dual of the graphic beta move.

I proved earlier the the extended beta move is equivalent with the pair (graphic beta move, dual of the graphic beta move), let me recall this pair in the following picture.

beta_beta_star

Here are some particular applications of the dual of the graphic beta move. The first is this:

beta_beta_star_1

But this is equivalent with the emergent algebra move R1a (via a CO-COMM move).  Likewise, another application of of the dual of the graphic beta move is this:

beta_beta_star_2

which is the same as   the emergent algebra move R2a.

The third application is this one:

 

beta_beta_star_3

 

and it was discussed in the post “Second thoughts on the dual of the extended beta move“, go there to see if this move may be interpreted as a pruning move (or an elimination of loops).

Finally, there is also this:

beta_beta_star_4

which was not mentioned before. It suggests that

beta_beta_star_5

behaves like the generic point in algebraic geometry.

Scarcity damages dissemination of knowledge

Here are two graphical illustrations of the process of dissemination of knowledge.

From the point of view of the author/researcher it looks like this:

s_race

From the point of view of those seeking knowledge it looks like this:

Brain_2

Then, obviously, from the point of view of the researcher  SCARCITY is a very bad idea.

Now, what?

Preparations for Christmas done, now in the mood for posting in my “dear diary” category (actually never been able to have one in the real world, excepting one try when I was 12, during a sea trip, which resulted in a meteo report).

Now, what? Let’s see:

1. With detached curiosity (because of an optimistic nature), I read that the agency which manages research grants here has been dismantled and a new organization of its activity will start soon (here, in Romanian).  Given my previous reactions, like those under this tag, I better have a plan B, right? So, is there anybody there interested in using my capacity to generate new ideas 😉 ? I anticipated this, some time ago, thinking about a job shelter, and even had some subconscious thoughts when I wrote  a professional wishlist.

2. I am very glad to have the occasion to learn a lot, this year, for example about some amazing ideas, like Digital Materialization, see also Carl Vilbrandt on google+. There are posts on this blog concerning digital materialization and eventual benefits of collaboration between DM and euclideon (which is not a scam, if there is still needed to mention).   “Now, what?” applies very well here, in the sense, that I am very curious to see if there is really any use of fractal image compression (type) algorithms for freps (and for the format euclideon uses), or what else is happening there?

3. Where is graphic lambda calculus going? For me it is firstly a proof of the fact that “computing with space” is a kind of computing (albeit I am still not convinced that “computing”  applies to the way the visual brain works). There are plenty of mathematical venues to explore, like: is there a pi-calculus version, a typed version, is the extended beta move reasonable, can it be used for real for computing,  and so on.

Most of all, what is this duality meaning? Is there a category theory fact, hiding in there, given that some typed lambda calculi (with eta reduction) admit a description in cartesian closed categories?

4. Will appear a Journal of very short papers?  Will publishers start to value peer-reviews? I am very excited about such ideas and my best hope is that the “global mind” of www users will come with much better ideas than a single “neuron” like me might have.

5. Although I changed the route less than a couple of years ago, I am still interested in sub-riemannian geometry and subjects alike. In fact, I am longing for some plain old fashioned research and article writing period on solid math subjects, after this crazy shift I took. However, I have no regrets, because I was right when I wrote, without any proof, about computing with space!

Conversion of lambda calculus terms into graphs

This is part of the tutorial “Introduction to graphic lambda calculus“.

Here is described the algorithm for converting untyped lambda calculus terms into graphs in GRAPH.  (Source used: Local and global moves on locally planar trivalent graphs, lambda calculus and lambda-Scale, arXiv:1207.0332 [cs.LO], section 3.)

 A. Terms in lambda calculus. We have an infinite list of variable names x, y, z, .... A term in untyped lambda calculus is obtained after the application of a finite number of times of any of the following:

  • variables are terms,
  • if A, B are terms then $AB$ is a term,
  • if x is a variable and A is a term then \lambda x. A is a term.

There are two operations:

  • the application, which sends a pair of terms (A,B) to the term AB,
  • lambda abstraction, sending a pair (x,A), made by a variable and a term, to the term \lambda x.A.

I shall therefore represent terms as syntactic trees. For the application operation I shall use the gate \curlywedge and for the lambda abstraction I shall use a gate decorated by a \lambda inscribed into a square.

syntrees

Notice that the gate for the lambda abstraction is not the \lambda gate from graphic lambda calculus.

Any term is represented as a binary tree, with nodes for the application and lambda abstraction operations and with leaves decorated by variable names.

I shall take as examples  the following five lambda terms: I = \lambda x . x, K = \lambda x. (\lambda y . (xy)), S = \lambda x . ( \lambda y . (\lambda z . ((xz)(yz)))) (the SKI combinators),  and other two famous terms, \Omega = (\lambda x. (xx)) (\lambda x. (xx)) and T = (\lambda x . (xy)) (\lambda x . (xy)).
B. Elimination of bound variables, part I.  Any leaf of the tree is connected to the root by an unique path. Start from the leftmost leaf, perform the algorithm explained further, then   go to the next leaf at the  right and repeat until all leaves are exhausted. We initialize also an empty list B of bound variables.

Take a leaf, say decorated with x \in X. To this leaf is associated a word,   denoted by w(x),  which is formed by the symbols of gates which are on the path which connects (from the bottom-up) the leaf with the root, together with information about which way, left (L) or right (R), the path passes through the gates. Such a word is formed by the letters \lambda^{L}\lambda^{R}\curlywedge^{L} and  \curlywedge^{R}.

If the first letter of the word w(x) is \lambda^{L} then add to the list  B the pair (x, w(x)) formed by the variable name x, and the associated word (describing the path to follow from the respective leaf to the root). Then pass to a new leaf.

Else continue along the path to the root. If we arrive at a \lambda abstraction gate, this can happen only coming from the right leg of the \lambda abstraction gate, thus we can find only the letter\lambda^{R}. In such a case look at the variable y which decorates the left leg of the same \lambda gate. If x =y then add to the syntactic tree a new arrow, from y to x and proceed further along the path, else proceed further. If the root is attained then pass to next leaf.

Examples: the graphs associated to the mentioned lambda terms,  together with the list of bound variables, are the following. (The added arrows are figured in red.)

  • The term I = \lambda x . x has associated list B = \left\{ (x, \lambda^{L}) \right\}, the term K = \lambda x . (\lambda y. (xy)) has  the list B = \left\{ (x, \lambda^{L}), (y, \lambda^{L} \lambda^{R}) \right\} and the term  S = \lambda x . ( \lambda y . (\lambda z . ((xz)(yz)))) has the list B = \left\{ (x, \lambda^{L}) , (y, \lambda^{L} \lambda^{R}) , (z, \lambda^{L} \lambda^{R} \lambda^{R}) \right\}. The syntactic trees with added arrows are:

step1_1

  • The term  \Omega = (\lambda x. (xx)) (\lambda x. (xx)) has the list B = \left\{ (x, \lambda^{L} \curlywedge^{L}) , (x, \lambda^{L} \curlywedge^{R}) \right\} and  the term T = (\lambda x . (xy)) (\lambda x . (xy)) has the list  B = \left\{ (x, \lambda^{L} \curlywedge^{L}) , (x, \lambda^{L} \curlywedge^{R}) \right\}. The syntactic trees with added arrows are:

step1_2

As you can see, there is a conflict of orientation of the red and black arrows. Therefore replace at this step the “square” gates of \lambda abstraction by the \lambda gates of graphic lambda calculus. Now the orientation of arrows is no longer conflicting.

C. Elimination of bound variables, part II.  The  list B  describes the bound variables. If the list is empty then go to the next step. Else, do the following, starting from the first element of the list, until the list is finished.

The variable name part of an element of the list, say the x from the pair (x, w(x)), is either connected to other leaves by one or more arrows added at step 1, or not. If it is not connected then erase the variable name with the associated path w(x)  and replace it by a termination gate.
If it is connected then erase it and replace it by a tree formed by \Upsilon gates, which starts at the place where the element of the list was  before the erasure and stops at the leaves which were connected to x. Erase all decorations which were joined to x and also erase all arrows which were added at step 1 to the leaf x from the list.

Examples: after the step 2, the graphs associated to the mentioned lambda terms  are the following.

  • the graphs of I, K, S are these:

step2_1

  •   the graphs of \Omega and T are

step2_2

Remark  that there may be more than one possible tree of gates \Upsilon, at each elimination of a bound variable (in case a bound variable has at least tree occurrences). One may use any tree of \Upsilon gates which is fit. The problem of multiple possibilities is solved by the CO-ASSOC move, in the sense that we may pass from one choice of a tree of \Upsilon gates to another by a succession of CO-ASSOC moves.

D. The last step. We may still have leaves decorated by free variables. Starting from the left to the right, group them together in case some of them occur in multiple places, then replace the multiple occurrences of a free variable by a tree of \Upsilon gates with a free  root, which ends exactly where the occurrences of the respective variable are. Again, there are multiple ways of doing this, but we may pass from one to another by a sequence of (CO-ASSOC) moves.

Examples: after the step 3,  all the graphs associated to the mentioned lambda terms, excepting the last one, are left unchanged. The graph of the last term, changes like in the right hand side of the following figure.

step3_2

We end up with graphs in GRAPH.

Peer-review turned on its head has market value

The comment by Peter Suber at the previous post “Journal of very short papers” made me realize that peer-reviewing free open access papers might have market value.  Provided that it is turned on its head.

Peter Suber points to the BMJ pico  publication model, which apparently is working for the medical community.  The idea is amazing, even more amazing is that it works.

BMJ publishes open access papers and sells one page abridged versions of the papers. Quote:

The full text of all accepted BMJ research articles is published online in full, with open access and no word limit, on bmj.com as soon as it is ready. In the print and iPad BMJ each research article is abridged, with the aim of making research more inviting and useful to readers.

More about the BMJ pico story here:  Abridgment as added value, SPARC Open Access Newsletter, issue #137 .

 

But what could be the use of an abridged paper for a math article? Those articles have abstracts, more abridged than this is hard to find. Yet, there is another abridged version of the mathematical article, of some sort. It is the peer-review report.

In the classical peer-review, things happen behind the scenes. When everything has the OK of the reviewers then the paper is published. The reports go to the trash bin.

Imagine now that some (benevolent hopefully) entity offers the paid service of selling (for tiny amounts of money, like songs are sold these days) the peer-reviews of articles from arxiv.

Instead of hiding the peer-review process and do it before publication, turn it on its head and sell it after the (free open access) publication. It might work, like the BMJ pico works. I think it works because it saves time for the researchers.

Emergent algebra moves R1a, R1b, R2 and ext2

This is part of the Tutorial:Graphic lambda calculus.

Here are described the moves related to emergent algebras. This moves involve the gates \bar{\varepsilon}, \Upsilon and the termination gate.

See the post “3D crossings in emergent algebras” in order to understand the relation with knot diagram crossings and with Reidemeister moves for oriented knot diagrams (for those I use the notations  from the paper    “Minimal generating sets of Reidemeister moves“,  by Michael Polyak  only that I use the letter “R” from “Reidemeister” instead of “\Omega” used by Polyak).

_________

We have an abelian group \Gamma with operation denoted multiplicatively and with neutral element denoted by 1. Thus, for any \varepsilon, \mu = \mu \varepsilon \in \Gamma their product is \varepsilon \mu \in \Gamma, the inverse of \varepsilon is denoted by \varepsilon^{-1} and we have the identities: 1 \varepsilon = \varepsilon , \varepsilon \varepsilon^{-1} = 1.

For each \varepsilon \in \Gamma we have an associated gate \bar{\varepsilon}.

  • The move R1a is described in the following figure

r1amove

The reason for calling this move R1a is that is related to the move R1a from Polyak paper (also to R1d). In the papers on emergent algebras this move is called R1, that is “Reidemeister move 1”.

  • The move R1b is this:

r1bmove

This move is related to the move R1b from Polyak (and also to R1c). This move does not appear in relation with general emergent algebras, it is true only for a special subclass of them, namely uniform idempotent quasigroups.

  • The move R2 is the following:

r2move

We shall see that this is related to all Reidemeister 2 moves (using also CO-ASSOC, CO-COMM, and LOCAL PRUNING).

  • The move ext2. The notation comes from the rule (ext2) from lambda-Scale calculus. In emergent algebra language it means that the emergent algebra operation indexed by the neutral element of \Gamma is the trivial operation xy = y.

ext2r

(but for this LOCAL PRUNING is also used).

___________________________

Return to Tutorial:Graphic lambda calculus