P1050219

Struktura słownika m 57

po prostu typy, które funkcjonują jako indeksy stałych i zmiennych. Reguły składni, zgodnie z którymi tworzy się typy, są także regułami generowania wyrażeń języka L„ — zob. (i), (ii), (iii).

Podstawowymi typami w języku L„ są typy następujące: t — typ indywiduum, o — typ wartości logicznej, fi typ możliwego świata.

Dziedziną zmiennej typu i jest uniwersum U, dziedziną zmiennej typu o jest zbiór wartości logicznych, a dziedziną zmiennej typu fi jest zbiór możliwych światów - W.

Klasa typów (T) zdefiniowana jest następująco:

(i) 1. | o, fteT

2.    Jeżeli typ asT i typ fteT, to typ złożony (aft)eT.

3.    Te i tylko te przedmioty są typami.

Jednostka (aft) uważana jest za funkcję określoną na zbiorze przedmiotów typu ft o wartościach w zbiorze jednostek typu a. Nawiasy wiążą od lewej, tj. ((((^ai)^a2)«3)^a*) można zapisać a, a₂ a₃ a₄ (a, ft są zmiennymi typów).

Rozważmy kilka przykładów. Na podstawie (i) t, oeT. A zatem oieT. Wyrażenie typu oi jest funkcją określoną na uniwersum U w zbiór wartości logicznych. Tak więc typ oi jest typem klasy. Analogicznie: typ oi/teT, gdyż także oieT. Typ oijj. jest typem własności indywiduum, tj. funkcją ze zbioru możliwych światów w zbiór klas elementów uniwersum U.

Szczególną cechą składniową języka jest to, że wyrażenia złożone tworzone są w nim za pomocą funkcji jednoargumentowych. Ponieważ nawiasy wiążą od strony lewej, wyrażenia języka powinny być odczytywane od prawej ku lewej, podczas gdy wyrażenia logiki pierwszego stopnia można odczytać od lewej ku prawej. Np. w klasycznej notacji relacji n-argumentowej zapisuje się R(A _t ... A„), podczas gdy w języku Ł będzie ona zapisana: ((R AJ ...) A,. W języku tym relacja n-argu-menlowa traktowana jest jako funkcja, która każdej jednostce typu cti, oznaczonej A,, przyporządkowuje relację (n—l)-argumentową, tj. ((R AJ ...)<4₂ (szczegóły — por. /5I).

Następną podstawową regułą składni w języku L_u jest (ii):

(ii) AB (AB) aft ft a

tj. jeżeli A jest wyrażeniem typu aft, zaś B jest wyrażeniem typu ft, to wyrażenie (A B) jest wyrażeniem typu a. Z semantycznego punktu widzenia oznacza to, że (A B) określa wartość funkcji oznaczanej przez wyrażenie A typu aft dla argumentu oznaczanego przez wyrażenie B typu ft.

Np. jeżeli C jest wyrażeniem typu oi (klasą indywiduów), a J — wyrażeniem typu i (indywiduum), wtedy wyrażenie (C₀,J.) jest wyrażeniem typu o, tj. odnosi się do wartości logicznej (która jest „prawdą”, jeżeli JsC).

Dalej, niech L będzie językiem typu oifi, w — zmienną możliwego świata typu H, zaś J — wyrażeniem typu i, jak wyżej. Zgodnie z (ii) możemy zapisać: które w konsekwencji należy do typu o, tj. oznacza wurtość logiczną zależną od