{"action":"created","issue":{"url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/13","repository_url":"https://api.github.com/repos/dylnb/LambdaCalculator","labels_url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/13/labels{/name}","comments_url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/13/comments","events_url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/13/events","html_url":"https://github.com/dylnb/LambdaCalculator/issues/13","id":145817615,"number":13,"title":"Predicate Modification brackets","user":{"login":"eecoppock","id":6325362,"avatar_url":"https://avatars.githubusercontent.com/u/6325362?v=3","gravatar_id":"","url":"https://api.github.com/users/eecoppock","html_url":"https://github.com/eecoppock","followers_url":"https://api.github.com/users/eecoppock/followers","following_url":"https://api.github.com/users/eecoppock/following{/other_user}","gists_url":"https://api.github.com/users/eecoppock/gists{/gist_id}","starred_url":"https://api.github.com/users/eecoppock/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/eecoppock/subscriptions","organizations_url":"https://api.github.com/users/eecoppock/orgs","repos_url":"https://api.github.com/users/eecoppock/repos","events_url":"https://api.github.com/users/eecoppock/events{/privacy}","received_events_url":"https://api.github.com/users/eecoppock/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/dylnb/LambdaCalculator/labels/question","name":"question","color":"cc317c"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-04-04T22:03:51Z","updated_at":"2016-04-05T00:29:19Z","closed_at":null,"body":"Hi,\r\n\r\nshouldn't\r\n\r\n`Lx.[⟪N⟫](x) & [⟪PP⟫](x)`\r\n\r\nin the attached screenshot rather be\r\n\r\n`Lx.[[⟪N⟫](x) & [⟪PP⟫](x)](x)]`\r\n\r\n?\r\n\r\nBecause the result becomes:\r\n\r\n`λx.[λx.[city(x)]](x) ∧ [λy.in(y,texas)](x)`\r\n\r\nwhich is somewhat confusing.\r\n\r\n![screen shot 2016-04-05 at 12 01 29 am](https://cloud.githubusercontent.com/assets/6325362/14265439/cc9fb116-fac1-11e5-9d1a-e558f516f182.png)\r\n"},"comment":{"url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/comments/205558509","html_url":"https://github.com/dylnb/LambdaCalculator/issues/13#issuecomment-205558509","issue_url":"https://api.github.com/repos/dylnb/LambdaCalculator/issues/13","id":205558509,"user":{"login":"dylnb","id":1175004,"avatar_url":"https://avatars.githubusercontent.com/u/1175004?v=3","gravatar_id":"","url":"https://api.github.com/users/dylnb","html_url":"https://github.com/dylnb","followers_url":"https://api.github.com/users/dylnb/followers","following_url":"https://api.github.com/users/dylnb/following{/other_user}","gists_url":"https://api.github.com/users/dylnb/gists{/gist_id}","starred_url":"https://api.github.com/users/dylnb/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dylnb/subscriptions","organizations_url":"https://api.github.com/users/dylnb/orgs","repos_url":"https://api.github.com/users/dylnb/repos","events_url":"https://api.github.com/users/dylnb/events{/privacy}","received_events_url":"https://api.github.com/users/dylnb/received_events","type":"User","site_admin":false},"created_at":"2016-04-05T00:29:19Z","updated_at":"2016-04-05T00:29:19Z","body":"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.\r\n\r\nBut 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."}}