Ocena rachunku lambda z udziałem cyfr kościelnych

Rozumiem, że liczba kościelna wygląda jak (... n razy ...) . Oznacza to nie więcej, niż „funkcja stosowanych razy do funkcji ”. $c_n$ $\lambda s. \lambda z. s$ $s\;z$ $s$ $n$ $z$

Możliwa definicja funkcji jest następująca: . Patrząc na ciało, rozumiem logikę tej funkcji. Jednak, kiedy zaczynam oceniać, utknąłem. Zilustruję to przykładem: $\mathtt{times}$ $\mathtt{times} = \lambda m. \lambda n. \lambda s. m \; (n\; s)$

\begin{aligned} (λ m . λ n . λ s . m (n s)) (λ s . λ z . s s z) (λ s . λ z . s s s z) \\ \to^{*} & λ s . (λ s . λ z . s s z) ((λ s . λ z . s s s z) s)) \\ \to^{*} & λ s . (λ s . λ z . s s z) (λ z . s s s z) \\ \to^{*} & λ s . λ z . (λ z . s s s z) (λ z . s s s z) z \end{aligned}

$\begin{align*} (\lambda m. \lambda n. \lambda s. m \; (n\; s))(\lambda s.\lambda z.s\;s\;z)(\lambda s.\lambda z.s\;s\;s\;z) \mspace{-4em} \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; ((\lambda s.\lambda z.s\;s\;s\;z)\; s)) \\ \to^*& \lambda s. (\lambda s.\lambda z.s\;s\;z) \; (\lambda z.s\;s\;s\;z) \\ \to^*& \lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \end{align*}$

Teraz w tej sytuacji, jeśli najpierw zastosuję $(\lambda z.s\;s\;s\;z)\;z$ , osiągnę pożądany rezultat. Jeśli jednak najpierw zastosuję $(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)$ , jak powinienem, ponieważ aplikacja jest skojarzona z lewej strony, otrzymuję zły wynik:

$\lambda s. \lambda z.(\lambda z.s\;s\;s\;z)\;(\lambda z.s\;s\;s\;z)\;z \to \lambda s. \lambda z.(s\;s\;s\;(\lambda z.s\;s\;s\;z))\;\;z$

Nie mogę tego dłużej zmniejszać. Co ja robię źle? Wynik powinien być $\lambda s. \lambda z.s\;s\;s\;s\;s\;s\;z$

lambda-calculus church-numerals

— codd
źródło

Liczby kościelne w początkowej kadencji są nieprawidłowe. 2 jest reprezentowane przez , a nie .

λ s . λ z . s (s z)

$\lambda s. \lambda z. s (s z)$

λ s . λ z . s s z

$\lambda s. \lambda z. s s z$

— Uday Reddy,

Myślę, że twoja redukcja jest prawidłowa (chociaż tylko ją spojrzałem). Na koniec nie możesz zastosować do , to nigdy nie pojawia się w tym terminie. to , nie . Funkcje w rachunku lambda przyjmują jeden argument; są one efektywnie curry : funkcja dwuargumentowa jest implementowana jako funkcja jednoargumentowa, która przyjmuje pierwszy argument i zwraca nową funkcję jednoargumentową, która przyjmuje drugi argument i zwraca wynik. $(\lambda z. s s s z)$ $z$ $\lambda z. f f z$ $\lambda z. (f f) z$ $\lambda z. f (f z)$

Popełniłeś ten sam błąd podczas definiowania cyfr Kościoła. Cyfra Kościoła dla opiera się na skomponowaniu funkcji razy. „Funkcja zastosowane razy do funkcji ” . Co napisałeś jest funkcja zastosowane razy do funkcji i wreszcie do , co nie wydaje mi się użytecznym okresie. $n$ $n$ $s$ $n$ $z$ $\lambda s. \lambda z. s (s ( … s \: z) … ))$ $s$ $n-1$ $s$ $z$

$2 \times 3$ jest zatem . Pozwolę ci sprawdzić, czy to redukuje do . $(\lambda m n s. m (n s)) (\lambda s z. s (s \: z)) (\lambda s z. s (s (s \: z)))$ $\lambda s z. s (s (s (s (s (s \: z)))))$

— Gilles „SO- przestań być zły”
źródło

Jeśli chodzi o akapit, masz rację i wiedziałem o tym. Po prostu uderzyło mnie, że zastosowanie odpowiednio asocjatywnego skutkuje właściwym rezultatem. Co do drugiego akapitu: masz rację. Nieużywanie nawiasów klamrowych było dla mnie błędne, ponownie ze względu na lewe skojarzenie aplikacji. Znowu zredukuję to wszystko i zobaczę, czy mój brak aparatu nie spowodował mojego błędu!

— codd

Tak się stało. Zauważasz, że moja notacja sugerowała niewłaściwą kolejność aplikacji rozwiązała problem! Akceptując twoją odpowiedź.

— codd