Lambda Rachunek

Question

Wszystko,

Poniżej jest wyrażenie lambda której jestem znalezienie trudno zmniejszyć to znaczy, że nie jestem w stanie zrozumieć, jak go o tym problemie.

(λm XN λa λb m (nab) b.) (Λ f x x.) (Λ f x fx).

To co próbowałem, ale siedzę:

Zważywszy powyższe wyrażenie a (. λf x x) (λm.E) m równa się
E = (. XN λa λb m (nab) b)
m = (. λ fx fx)

= > (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

C stwierdzenie powyższego wyrażenia jako (λn. E) M odpowiada
E = (λa λb. (Λ f x. X) (λ f x. F x) (n a b) b)
M = ??

.. i jestem zagubiony !!

Czy ktoś może mi pomóc zrozumieć, że dla JAKIEGOKOLWIEK wyrażenia lambda, jakie kroki należy wykonać, aby zmniejszyć?

Answer 1

można wykonać następujące kroki w celu zmniejszenia wyrażeń lambda:

1. Pełne sformatowanie wyrażenia, aby uniknąć błędów i sprawić, że stanie się bardziej oczywiste, gdzie ma miejsce funkcja aplikacji
2. Znajdź aplikację funkcji, tj. Znajdź wystąpienie wzorca (λX. e1) e2, gdzie X może być dowolnym poprawnym identyfikatorem, a e1 i e2 może być dowolnym poprawnym wyrażeniem.
3. Zastosuj funkcję zastępując (λx. e1) e2 z e1' gdzie e1' jest wynikiem zastąpienia każdego wolnego wystąpienie x w e1 z e2.
4. Powtarzaj 2 i 3, aż wzór przestanie występować. Należy pamiętać, że może to prowadzić do nieskończonej pętli do wyrażenia non-normalizacji, dlatego należy przerwać po 1000 iteracji i tak ;-)

Tak dla przykładu możemy zacząć od wyrażenia

((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x))) 

Tutaj podwyrażenie (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x)) pasuje do naszego wzoru z X = m, e1 = (λn. (λa. (λb. (m ((n a) b)) b)))) i e2 = (λf. (λx. x)). Więc po podstawieniu otrzymujemy (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))), co sprawia, że ​​całe nasze wyrażenie:

(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x))) 

Teraz możemy zastosować wzór dla całego wyrażenia z X = n, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) i e2 = (λf. (λx. (f x))). Więc po podstawieniu otrzymujemy:

(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b)) 

Teraz ((λf. (λx. (f x))) a) pasuje do naszego wzorca i staje (λx. (a x)), co prowadzi do:

(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b)) 

Tym razem możemy zastosować wzór do ((λx. (a x)) b), co zmniejsza do (a b), co prowadzi do :

(λa. (λb. ((λf. (λx. x)) (a b)) b)) 

teraz zastosować wzór do ((λf. (λx. x)) (a b)), co zmniejsza do (λx. x) i otrzymaj:

(λa. (λb. b)) 

Teraz skończyliśmy.

Answer 2

Gdzie idziesz złego jest to, że w pierwszym etapie, nie można mieć

M = (λf x. x)(λ f x. f x) 

ponieważ oryginalny wyraz nie obejmuje tego wyrażenia aplikacji. Aby to jasne, można umieścić w ukrytych nawiasach następujące zasady, że aplikacja jest lewy-asocjacyjne (używając [i] dla nowych parens i oddanie w niektórych brakuje s „”):

[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x) 

Stąd , znajdź wyraz formy (λv.E) M gdzieś wewnątrz i zmniejsz go, zastępując v przez M w E. Uważaj, że to naprawdę jest zastosowanie funkcji M: nie jest tak, jeśli masz coś takiego jak N (λv.E) M, ponieważ wtedy N jest stosowane do funkcji i M jako dwa argumenty.

Jeśli nadal tkwisz w martwym punkcie, spróbuj wstawić parens dla każdej lambdy - w zasadzie nowy "(" po każdym "." I dopasowanym ")", który idzie jak najdalej w prawo, . Dopasowanie nowego „(” Jako przykład, zrobiłem je tutaj (używając [i], aby je wyróżnić):

((λm . λn . λa . [λb . m (n a b) b]) (λ f x. x)) (λ f x. f x)