ishanpm / chemlambda-editor

Javascript implementation of Chemlambda
MIT License
3 stars 0 forks source link

Complete model of lambda calculus #11

Open ishanpm opened 5 years ago

ishanpm commented 5 years ago

This isn't an issue with this editor, so much as Chemlambda itself. In its current form, there are many things it can do, but unfortunately being a complete model of lambda calculus is not one of those things. I would like to make an alternate version that can model every term properly.

The fundamental problem is that FI and FOE nodes are created in pairs when an L node is replicated, but they don't always meet up properly. Namely, whenever an abstraction uses a variable from an outer abstraction, the FOE from the former will interrupt the FI from the latter. Here are some potential solutions:

  1. Have an actual link between FI and FOE. This would make the link completely explicit. However, when FOE nodes are duplicated, those links will have to do some weird tricks to stay straight.
  2. Make entering a lambda abstraction explicit. This involves an additional two-valent node called B for barrier. FO and FOE are generalized to a single FO node with a natural number associated with it. If the number is zero, then it acts like a regular FO, otherwise it acts like FOE. The number is incremented when crossing an L, and decremented when crossing a barrier. This doesn't have to be an actual number associated with the node, it could be represented using an arrangement of nodes near/on the FO. After an L-A move, all barriers corresponding to that L must be removed.

Both of these solutions would involve a lot of extra transitions to accommodate the extra layer of information. I wonder if there's a simpler way?