3148972485

Wartości logiczne

Specyfikacja algebraiczna:

if true M N — M    if false M N — N

Odpowiednie termy można zdefiniować na przykład tak:

true = \xy.x false = Axy.y    if = \buv.buv (-»^ A6.6)

Udowodnimy, że spełnione jest pierwsze równanie specyfikacji.

if true M N = (\buv.b u v) true M N —(Aiw.true u v)M N —>p (A^.true M v) N    —>p true M N

=    (\xy.x) M N    —>p (Ay.M)N

~>t3 M

Analogicznie wygląda dowód drugiego równania.

W celu zwiększenia czytelności czasem zamiast if B M N będziemy pisali if BthenMelseN.

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