Log in

No account? Create an account
Woke up early this morning with severe gut distress. Hope it wasn't… - Notes from a Medium-Sized Island [entries|archive|friends|userinfo]

[ website | My Website ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

[Feb. 15th, 2016|09:09 pm]
[Tags|, ]

Woke up early this morning with severe gut distress. Hope it wasn't anything in particular I ate yesterday. Felt better later on in the evening. Still find myself unable to stop thinking during free moments about this lambda-term-graph correspondence thing.


(Deleted comment)
[User Picture]From: jcreed
2016-02-17 01:33 am (UTC)
The undirected graphs are just all of the undirected graphs. Or, uh, technically, all of the "rooted planar maps", with zero edges, one edge, two edges. "Rooted" is the fact that you have to pick a half-edge poking out of some vertex toward the outside of the map. Because of the planarness of everything, exactly which other edges the root is wedged between actually matters --- you're not allowed to swap around edges the way you could with an abstract graph, nor flip everything over. Rows 4 and 9 following the last black line are mirror images of one another, but they're considered distinct.

The weird thing that http://arxiv.org/pdf/1408.5028.pdf proves is that the number of closed, normal, ordered-linear lambda terms with n lambdas (not pictured at all above! there's lots of beta-redices) is exactly https://oeis.org/A000168 the number of rooted planar maps. And I haven't yet grokked the proof in the paper, so I was searching around for some other way to understand it from scratch.

There ought to be a proof that there's a bijection between closed (ordered) terms of the syntactic class E in that picture, and closed normal ordered-linear lambda terms, but danged if I can figure out what it is. It seems like it has to involve some long-range reaching into the variable bound by various lambdas and case-analyzing what context it occurs in, which should come as little surprise, since the proof in the noam-paper does a bunch of stuff like that I think.

Edited at 2016-02-17 01:36 am (UTC)
(Reply) (Parent) (Thread)