Document meaning of alpha/beta functions about abstracttext HOT 15 OPEN

Hmm, interesting how lamda's α-conversion and β-reduction ideas seem to show up in other places, like in String replace functions.

(α-conversion)
replacement function with a String replacement mapping of variables held in an array:
http://commons.apache.org/proper/commons-lang/apidocs/org/apache/commons/lang3/StringUtils.html#replaceEach-java.lang.String-java.lang.String:A-java.lang.String:A-
StringUtils.replaceEach("abcde", new String[]{"ab", "d"}, new String[]{"d", "t"}) = "dcte"

(β-reduction)
repeatedly applying a replacement function with arguments:
http://commons.apache.org/proper/commons-lang/apidocs/org/apache/commons/lang3/StringUtils.html#replaceEachRepeatedly-java.lang.String-java.lang.String:A-java.lang.String:A-
StringUtils.replaceEachRepeatedly("abcde", new String[]{"ab", "d"}, new String[]{"d", "t"}) = "tcte"

from abstracttext.

Thad, yes, it is both are based on lambda calculus' use of the terms.

from abstracttext.

Maybe. Or any other lexer and parser generator.

For the function call syntax in eneyj itself it's overkill.

For the other languages I would leave that choice to whoever implements it :)

Both for Python and JavaScript, I would think that the built-in parsers for Python and JavaScript might be good choices without introducing external dependencies.

from abstracttext.

The global alpha and beta are defined in src/evaluate/_evaluate.js, and each load the evaluator (a JS module) for the data argument’s type, and then call that evaluator’s alpha or beta function. Each evaluator defines its own alpha and beta functions (many, but not all, also define an evaluate function), which is apparently where some of the work of evaluation happens.

As far as I can see, the global alpha and beta are mainly called by the individual alpha and beta functions; the only “entry point” from outside that I’ve seen so far is the evaluate function for Z7, functioncall, which (very roughly speaking) appears to call the global alpha on the call target, and the global beta on each argument.

from abstracttext.

I also remember from university that lambda calculus has a β-reduction operation, which could be related. In those classes, the closest α “thing” was α-equivalence, wherein two expressions are α-equivalent if you can validly rename one into the other, e. g. (λx. λy. x y) is α-equivalent to (λy. λx. y x) but not to (λx. λx. x x) – this didn’t seem to match eneyj’s alpha very well. But I just looked at the Wikipedia article, and there this is described as an α-conversion, which is the operation of renaming a lambda in this way. So it sounds like eneyj’s alpha and beta might map to lambda calculus’ α-conversion and β-reduction: alpha is related to renaming, and β reduces an object by replacing references to a name with a value for that name.

I still don’t understand the alpha signature, though. There’s the data object, a variable name, and a GUID. What is being renamed to what else here?

from abstracttext.

Okay, looking at src/evaluate/Z18.js helps a lot (Z18 is argument_reference).

• When alpha-converting an argument reference with a matching variable name that doesn’t have a GUID yet, return a new argument reference with the given GUID.
• When beta-reducing an argument reference with a matching variable name, return the given value only if its GUID matches the given GUID.

Effectively, the alpha function binds all unbound references to a variable name to a certain GUID; a reference is unbound if it doesn’t have a GUID yet.

So it’s not really that something is being renamed to something else, but rather that a reference has two names: a variable name (I want to call this a “symbolic name”) and a GUID. It starts out with just the variable name, and alpha conversion assigns it a GUID; later, beta reduction inspects the GUID to see if the reference really refers to the same variable or if there has been a name collision.

At least, that’s what I think so far.

from abstracttext.

Lucas, yes, that's exactly it.

alpha is alpha conversion, beta is is beta reduction, and Z7 evaluation should be the only entrypoint to both alpha and beta.

(Furthermore I would hope I could get rid of most of the individual alpha and beta implementations - Z200 and Z2 really shouldn't have alpha, beta, or evaluate functions, they should be handled by the global alpha, beta, or evaluate functions. This is not true for Z18 and Z7).

alpha conversion makes sure that two variables don't collapse just because they have the same name. It doesn't touch unbound variables, but binds every bound variable to a GUID (which is the true identity of the variable). This is particularly relevant for recursive calls.

beta reduction then replaces all variables with the respective values of the relevant argument, i.e. it turns add(x,y)(5) into add5(y), or add(x,y)(5,2) into 7. At this point, this works over the GUIDs, as these are the true identities of the variables, not the symbolic names (which are still needed for debugging etc.)

I agree that this should be documented somewhere, I am just not sure where. Would you have preferred a document in docs or should it be in the global evaluation function? Or in one of the local functions?

Thanks for going so deep into the rabbit hole, I really appreciate it!! This will help with getting the code to become much more accessible.

from abstracttext.

I think a comment above the alpha and beta functions in eneyj/src/evaluate/_evaluate.js would be a good place for at least a brief description of the functions.

I also wonder if evaluation has to work in this way, or if it’s possible to achieve the same results in different ways. I’ll hopefully explore this in my Graal implementation (still extremely WIP).

from abstracttext.

Good idea, will do with the comments.

I actually don't think evaluation has to work that way. It might be entirely possible that evaluation can work in a much different way, something more intuitive to a programmer born after 1950, that is not relying on an actual implementation of Lambda Calculus. But every time I try to think of it, I get something akin to a buffer overflow (which also might be due to me not having really me-time currently, so I can't think about it for it for a longer time).

Basically something that just evaluates a function call in its entirety (and then recursively) instead of looping through each of the variables doing replacement and reduction. I think that might lead to a much easier to understand codebase.

from abstracttext.

I added some documentation:

d191015

8edc0c4

Let me know if that makes sense by closing this issue, or offer feedback on how to improve it.

By the way, I think one of the reasons why it is using lambda calculus is that originally the code was able to deal with arbitrary number of arguments and arbitrary number of parameters. So you could call a two-argument function with a single parameter. It is possible that this is now not possible anymore as validation might stop that. But this was helpful with the original implementation of the core lambda calculus, which now got hidden behind Z40 lambda type. All Z40s originally were Z8 but in order to have stronger validation I turned them into a new type Z40. Z39 lambda to function is the magic that takes a Z40 and turns it into the Z8 it usually was.

This allowed to write the Z40 at a higher level of abstraction.

But this also might mean that we actually do not need to go through a lambda calculus implementation anymore, but can do something easier to understand. I don't know.

from abstracttext.

@vrandezo have you considered establishing a mailing list to discuss things in more detail? Until then I guess github issues provide a forum for us ...

So, it seems to me what you're doing here is defining a programming language and the tools for interpreting/compiling it (at least turning it into javascript). I'm not super-familiar with compiler design, but I think the parsing step (after tokenizing) generates a "syntax tree"; the eneyj json format(s) I think is making that tree more explicit than usual (with json providing built-in serialization/deserialization). Given enough richness in the basic functions, I would assume that code in any (functional?) programming language could be turned into an eneyj tree; that would require parsers for those languages of course.

Would the reverse be possible? There might need to be some more provision for storing variable names (a symbol table?) but what if you could turn eneyj code into your favorite programming language (from some limited list) and back again, so that the wiki editing function was basically a code editor in python, haskell, clojure, whatever (or the raw json if you really want)? That's sort of the wiki dream I had for this project, but it may be too farfetched??

from abstracttext.

A mailing list is probably a good idea. The one thing that has prevented me from doing it so far is naming the list and where to put the mailing list :)

At least the Github issues are also public and archived for now.

I am sometimes wary of calling it a programming language (here for example), and sometimes I totally do it (here for example). So one could reasonably say that I should get my act together about this. I think it is not really a programming language because it doesn't have a real syntax, and it relies in most cases on implementations in other programming languages for grounding. Maybe the best way to call it is to call it an abstract programming language, but that's getting very inception...

LISP is similar in that way that it represents an explicit syntax tree.

So, now, if we look at it as an abstract programming language, then your suggestion makes a lot of sense. And in fact one could do that - but there are a few caveats: there are three major contributions by these programming languages, and their abstraction is actually quite difficult in detail.

1. Syntax. eneyj currently only allows a function-call syntax, and that's it. Programming languages have rich syntactic structures, such as operator precedence, infix-operators, syntax for literals, etc. All of these would need to be translated back and forth in order for this to work. That would be work, but I think I would think that would be quite fun. It would also help with ensuring the security of the system (i.e. something like this would make the safety model of eneyj much easier to implement)

2. Libraries. The power of most programming languages come from their libraries. This is also very valuable to preserve, but this would need to somehow lift out of eneyj. This could probably be done in some way by annotating Z-Functions to standard library implementations, but this would also mean to copy their specifications over to eneyj. This would be a lot of detailed work.

3. Type system. And stuff like conversion, coercion, subtypes, dispatching, type composition, etc. Currently, eneyj doesn't support any of these. And the type system between languages often differs in the details, which would make this hard.

So, in short, yes, this would be awesome. The easiest way to do is, and to start this, is to create a parse function (ideally in eneyj) that takes a string and returns an implementation, and a linearizer that takes an implementation and returns a string. And the string is that particular implementation in that given language. And then work away all the problems that show up, but I would worry about them on the way. And I would start with a restricted sublanguage, and then extend this until it eventually captures the whole language.

The great benefit is that this is immediately beneficial as it allows to reuse skills by contributors and as it allows us an explicit path to security, because once we translate a string of python code into an eneyj implementation zobject, well, we know what it is doing and whether it is safe.

Regarding variables: so far, I avoided them, because they can be avoided. Also statements. But programming in most languages needs variables and statements. In order to support these, I am not sure how to best proceed, but this would probably require a bigger transformation, and I don't know if that would be reversible to get back to the original string. Hmmm. We need to think about this more.

from abstracttext.

Hmm, I'm wondering if ANTLR4 might have a place here to help generate the lexer and parser?

from abstracttext.

Definitely this is a bit tricky to even wrap your brain around... I had a very rough idea of starting with something like Peter Norvig's python lisp interpreter - https://norvig.com/lispy.html - even the first "Lispy Calculator" piece, but that already pulls in things that are not yet available in eneyj - float literals, and the "math" library (though all that's really used from that is the number "Pi"). Otherwise though it's an extremely simple language that at least allows us to define variables and use conditionals ...

from abstracttext.

Re @arthurpsmith : But that's for the semantics of the functions, not for tokenizing and parsing. It should be possible to implement the parser and then hand over the actual functions to Z-Function with implementations that could very well be in python and thus use math.pi etc.

from abstracttext.