library(lambda): Terminology/Consistency

[triska]

We currently have "parameter" and "argument" denoting apparently the same concept:

https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/lambda.pl#L61

https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/lambda.pl#L86

https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/lambda.pl#L219

https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/lambda.pl#L227

https://github.com/mthom/scryer-prolog/blob/d6ac03552d8484f8ad7c4307d1c9cfb5db46b16f/src/lib/lambda.pl#L233

Any thoughts?

[UWN]

For argument, see 3.7. A compound term has arguments. A goal has arguments similarly.

A parameter, more specifically a lambda parameter, is not an argument (or, strictly speaking it is the first argument of (^)/2when used in a fitting context). But with (^)/3..10 it is connected ("passed") to an argument.

[triska]

Thank you a lot!

Specifically, in the following example:

?- X+\(X=a).
   X = a.

Would we say that (X=a) is a lambda expression with no parameters? It appears so! (I mean, taking into account 3.7, it does seem to fit better than "no arguments").

Yet the documentation also states "...the result of an insufficient number of arguments". "Parameter" does not seem to fit in this specific case, but "argument" also seems to not completely fit if we stick to just 3.7.

Moreover, I get for example:

?- t+\X^(true).
   error(existence_error(lambda_parameter,lambda:user:_474^true),_463).

But in fact a parameter (namely X) does exist! It overexists, in a sense. What is lacking here? In the terminology of the documentation quoted above, the argument?

[UWN]

?- X+\(X=a).

No parameters. Only renaming of variables (in this case none) within the goal.

Note that λ is deconstructed to \ and ^. The ^ is responsible for parameter passing, whereas the \ is here for renaming.

?- t+\X^(true).
   error(existence_error(lambda_parameter,lambda:user:_474^true),_463).

Just the same with

?- inex.
   error(existence_error(procedure,inex/0),inex/0).

In logic there is no fundamental difference between a goal and its definition. It is rather the viewpoint of a programming language that we interpret a goal as something that "expects" an explicit definition at the point in time of its execution. And thus we conclude that it's existence is missing. We could equally say that the goal is bad and it is good that that predicate does not exist. Think of a typo. But still we describe this error only by implicitly assuming that the goal is right and the definition is wrong when quite often it is the other way around.

Same for the lambda parameters. We have provided too many such parameters and thus some of them can no longer be actually used as parameters by call/N. So are they parameters at all? Or, we have used that expression incorrectly by expecting less arguments, so the caller is the culprit. I'd say, get used to it in the same manner the existence errors are often typos.

What irritates me more is the superfluous lambda: prefix. It is produced because a meta argument is copied (in Scryer with copy_term_nat/2) and thus the new variable appears as something that needs to be prefixed. Not sure how to fix this in a clean manner. Probably not worth fixing since all should be expanded away (after expansion, the inverse of preparation for execution and all that gets settled).