Predicate Modification brackets

[eecoppock]

Hi,

shouldn't

Lx.[⟪N⟫](x) & [⟪PP⟫](x)

in the attached screenshot rather be

Lx.[[⟪N⟫](x) & [⟪PP⟫](x)](x)]

?

Because the result becomes:

λx.[λx.[city(x)]](x) ∧ [λy.in(y,texas)](x)

which is somewhat confusing.

[dylnb]

Lx.[[⟪N⟫](x) & [⟪PP⟫](x)](x)] has what looks to me like an extra (x)] at the end. Did you mean to suggest Lx.[[⟪N⟫](x) & [⟪PP⟫](x)]?

[eecoppock]

Yes.

On Tue, Apr 5, 2016 at 1:03 AM, Dylan Bumford notifications@github.com wrote:

Lx.[⟪N⟫](x) & [⟪PP⟫](x)] has what looks to me like an extra (x)] at the end. Did you mean to suggest Lx.[⟪N⟫ & ⟪PP⟫]?

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/dylnb/LambdaCalculator/issues/13#issuecomment-205534527

Elizabeth Coppock, Ph.D., Docent in Linguistics Pro Futura Scientia Fellow Swedish Collegium for Advanced Study (SCAS), Uppsala, Sweden Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg http://eecoppock.info

[dylnb]

The current calculator convention is to bracket redex heads, parenthesize redex args, and not to add vacuous delimiters otherwise. Given that we're adhering to the standard syntactic principle that binders scope as far to the right as possible, the calculator doesn't add brackets around the conjunction [N](x) & [PP](x) because it's understood to be in the scope of the lambda, and not the head of any redex. Likewise, the next step λx.[λx.[city(x)]](x) ∧ [λy.in(y,texas)](x) may be a little hard to look at, but it's not ambiguous: the outer lambda scopes over everything, and then it's just two []() redices joined by conjunction.

But I guess the issue here is that it can be confusing to mix the practice of bracketing the body of the lambda term --- e.g. λx.[city(x)] --- with the practice of bracketing the entire function term (if it's the head of a redex). Since the semantics of the calculator follows the latter practice, I would have thought it'd be better not to generate body brackets as if it followed the former. Of course your example shows that an outermost lambda can end up next to what look like scope-delimiting brackets anyway, if the leftmost subterm of the body happens to be a redex. I can look into trying to generate whole-body brackets only in this case, so as to try and stave off confusion for people intent on using brackets to delimit the scope of the lambda. But I think my pedagogical position would be that if a user thinks λx[P(x)](j) will reduce to P(j) --- or in this case, that λx.[λx.[city(x)]](x) ∧ [λy.in(y,texas)](x) will reduce to the ill-formed [λx.[city(x)]] ∧ [λy.in(y,texas)](x) --- it would be better for them to see that it does not, and to learn the rules the way the tool understands them, than for us to try and anticipate all the ways that a person with a different semantics for the lambda calculus might get tripped up, and to generate alternative terms that mean the same thing in both dialects.