Rozumiem, że liczba kościelna wygląda jak (... n razy ...) . Oznacza to nie więcej, niż „funkcja stosowanych razy do funkcji ”. λ s . λ z . s ss 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:t i m e s = λ m . λ n . λ s . m
Teraz w tej sytuacji, jeśli najpierw zastosuję , osiągnę pożądany rezultat. Jeśli jednak najpierw zastosuję , jak powinienem, ponieważ aplikacja jest skojarzona z lewej strony, otrzymuję zły wynik:
Nie mogę tego dłużej zmniejszać. Co ja robię źle? Wynik powinien być
Odpowiedzi:
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.oo λ oo . f f z λ z . ( f f ) z λ z . f ( f z )( λ z. s s s oo) z λ z. fafaz λ z. ( ffa) z λ z. fa( fz)
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 s n z λ s . λ z . s ( s ( … sn n s n z s n - 1 s zλ s . λ z. s ( s ( … sz) … ) ) s n - 1 s z
źródło