Является ли λxyz.xz (yz) абстракция или приложение в Lambda Calculus? - PullRequest
Новая
       6

Является ли λxyz.xz (yz) абстракция или приложение в Lambda Calculus?

0 голосов
/ 15 апреля 2019

Согласно лямбда-исчислению, λxyz.xz(yz) следует рассматривать как применение от λxyz.xz до (yz) или делать скобки в xz(yz), что означает, что операции должны идти как (xz)(yz) вместо ((xz)y)z и* * * * * * * * * * * * * * * * * * * *

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * -

* Я полагаю, что это абстракция, и вместо этого приложение должно быть написано как (λxyz.xz)yz, но мое понимание очень плохое, поэтому я подумалаЯ бы проверил.

1 Ответ

0 голосов
/ 15 апреля 2019

Правильно.Чтобы быть точным, это зависит от точного определения синтаксиса лямбда-терминов, точнее, правил для исключения скобок, но для этих правил есть соглашение.В частности, обычно приложение

  • имеет приоритет над абстракцией , поэтому сначала вы пытаетесь сформировать приложение от xz до yz, и только затем абстракции над x, y и z вместо того, чтобы сначала формировать абстракцию λxyz.xz, а затем встраивать результирующий термин в приложение к yz (это то, что вы получили бы, если бы абстракция имела приоритет над приложением);
  • брекетинг в терминах приложения является ассоциативным слева, поэтому xzyz (без скобок вокруг yz) будет читаться как ((xz)y)z, а чтобы указать, что xz применяется к yz, необходимо заключить в скобкитермин yz.

Итак, как вы подозреваете, λxyz.xz(yz) - это трехкратная абстракция над xz(yz), которая сама является приложением от xz до yz, которыеснова приложения от x до z и y до z, соответственно.

При наличии всех скобок термин λx.(λy.(λz.(xz(yz)))).
Синтаксическое дерево для термина выглядит следующим образом: 

λxyz.xz(yz): abstraction
|- x: variable
|- λyz.xz(yz): abstraction
  |- y: variable
  |- λz.xz(yz): abstraction
     |- z: variable
     |- xz(yz): application
        |- xz: application
        |  |- x: variable
        |  |- z: variable
        |- yz: application
           |- y: variable
           |- z: variable

И, как вы правильно подозреваете, приложениеот λxyz.xz до yz будет записано как (λxyz.xz)yz.

...