3148972476

Reguły delta

Przykład: test na zero

W wielu funkcjach konieczne jest sprawdzenie, czy liczba jest równa zeru. Specyfikacja takiego predykatu wygląda następująco:

f    isZero 0 = true

\ isZero (sucn) = false

Spełnia ona wymagania twierdzenia z poprzedniej strony ( przy założeniu, że n oznacza term zamknięty), więc moglibyśmy dodać do A-termów stałą isZero oraz dwie reguły redukcji, nie troszcząc się o znalezienie termu, spełniającego powyższą specyfikację.

My jednak podamy ten term.

isZero = An.lter n (A&.false) true

Łatwo pokazać, że spełnia on powyższą specyfikację. Analogicznie należy rozumieć następny przykład.

Zdzisław Spławski: Teoretyczne Podstawy Języków Programowania, Wykład 4. Siła wyrazu rachunku A 14