Issue with Demorgan Definition of AND

[stevenhuyn]

Thank you for the project! Was super fun!

I tried defining AND in terms of NOT and OR and my definition does not seem to work. I believe this to be a bug? https://en.wikipedia.org/wiki/De_Morgan's_laws

AND:=λab.NOT(OR(NOTa)(NOTb))
AND: λa.λb.(λa.λb.λc.acb)((λa.λb.a(λa.λb.a)b)((λa.λb.λc.acb)a)((λa.λb.λc.acb)b))
<assignment>

> AND FALSE FALSE
λb.λc.c
<function, church numeral 0, church boolean false>

> AND FALSE TRUE
λb.λc.c
<function, church numeral 0, church boolean false>

// This case here doesn't seem to evaluate properly?
> AND TRUE FALSE 
λb.λc.b
<function, church boolean true>

> AND TRUE TRUE
λb.λc.b
<function, church boolean true>(+)

[evinism]

Tried doing this myself, defining NOT and OR, with

TRUE := λab.a
FALSE := λab.b
NOT:=λa.a FALSE TRUE
OR := λab.a TRUE b

This one copied from your issue above,

AND:=λab.NOT(OR(NOTa)(NOTb))

Seems to give me a proper AND:

> AND FALSE FALSE
λa.λb.b <function, church numeral 0, church boolean false>
> AND FALSE TRUE
λa.λb.b <function, church numeral 0, church boolean false>
> AND TRUE FALSE
λa.λb.b <function, church numeral 0, church boolean false>
> AND TRUE TRUE
λa.λb.a <function, church boolean true>

Trying this out with NOT:=λa.λb.λc.acb, I can recreate the issue you've found. Something's very fishy indeed.

[stevenhuyn]

Ah my bad on not giving the other defs

[evinism]

Reproducing fails with NOT:=λm.λn.λo.mon, which should be equivalent. Some naming issue pops up

[evinism]

These should be equivalent, but they execute differently:

[evinism]

Yikes, dependent on both a name collision in the automated alpha conversion and the target variable. (Middle is incorrect)

[evinism]

Reproducing in the spec: https://github.com/evinism/lambda-explorer/pull/127

[anderium]

Let's analyse it, under the preface that I didn't actually run any of this and it's purely manual code analysis.

To be on the same page, the issue is that spec occurs with this piece of AST:

{
  type: "function",
  argument: "b",
  body: { type: "variable", name: "b" },
}

This function does not contain $\epsilon_1$, so this will not lead to any collisions, but the $\alpha$-reduction cannot know this ahead of time. (Or at least, shouldn't have to.) (The case where it does contain $\epsilon_1$ is actually already handled correctly.)

In the capture avoidance step it then has to generate a new name. As far as the system is concerned, the free variables are:

const freeInReplacer = ["b"];  // The outer variable that the lambda is applied to.
const freeInExpressionBody = ["b"];  // This is actually not true, but irrelevant to this specific issue.
const argNames = [];

Using these variables, it thinks the first safe free name is $\epsilon_1$, so changes the alphaSafeExpression to

{
  type: "function",
  argument: "ε₁",
  body: { type: "variable", name: "ε₁" },
}

However, the resursive application of the reduction on the body of the alphaSafeExpression then updates the $\epsilon_1$ value.

https://github.com/evinism/lambda-explorer/blob/0fd8e7c5c482d54260c7f9832c4fc956b0c8bf82/src/lib/lambda/operations.ts#L138

So in addition to the three cases already mentioned, there is a fourth requirement that arguments should not change to the name you are trying to replace. As mentioned, if that name does occur in the body of the function it already works; it will appear in the freeInExpressionBody array.

https://github.com/evinism/lambda-explorer/blob/0fd8e7c5c482d54260c7f9832c4fc956b0c8bf82/src/lib/lambda/operations.ts#L112-L115

        // 4: isn't the argument name that is being replaced.

I.e. solved by adding nameToReplace into the array created here:

https://github.com/evinism/lambda-explorer/blob/0fd8e7c5c482d54260c7f9832c4fc956b0c8bf82/src/lib/lambda/operations.ts#L120-L122

        let newName = generateNewName(
          freeInReplacer.concat(freeInExpressionBody, argNames, [nameToReplace])
        );

It may also be solved by not doing any replacement at all if nameToReplace does not occur in the freeInExpressionBody array.

So why did I say that freeInExpressionBody is wrong?

The variable `b` is obviously bound in the function. This line should probably use `expression` instead of `expression.body`. https://github.com/evinism/lambda-explorer/blob/0fd8e7c5c482d54260c7f9832c4fc956b0c8bf82/src/lib/lambda/operations.ts#L116 Although in that case, the variable should be part of `argNames`, so that line should also use `expression` instead of `expression.body`. And unsurprisingly that should lead to the same result, only shifting the array in which the function argument itself occurs. https://github.com/evinism/lambda-explorer/blob/0fd8e7c5c482d54260c7f9832c4fc956b0c8bf82/src/lib/lambda/operations.ts#L119