Binarna logika kombinacyjna - Binary combinatory logic

Binarna logika kombinacyjna ( BCL ) to język programowania komputerowego , który wykorzystuje terminy binarne 0 i 1, tworząc pełne sformułowanie logiki kombinatorycznej przy użyciu tylko symboli 0 i 1. Używając kombinatorów S i K, można tworzyć złożone funkcje algebry logicznej. BCL ma zastosowanie w teorii złożoności rozmiarowo-programowej ( złożoność Kołmogorowa ).

Definicja

Podstawa SK

Wykorzystując kombinatory K i S logiki kombinatorycznej , funkcje logiczne mogą być reprezentowane jako funkcje kombinatorów:

Lista operacji logicznych jako kombinatorów binarnych
Algebra Boole'a Podstawa SK
Prawda(1) K(KK)
Fałsz(0) K(K(SK))S
ORAZ SSK
NIE SS(S(S(S(SK))S))(KK)
LUB S(SS)S(SK)
NAND S(S(K(S(SS(K(KK))))))))S
ANI S(S(S(SS(K(K(KK)))))(KS))
XOR S(S(S(SS)(S(S(SK)))S))K

Składnia

Postać Backusa-Naura : 

 <term> ::= 00 | 01 | 1 <term> <term>

Semantyka

W denotational semantyka Bcl może być określona w następujący sposób:

  • [ 00 ] == K
  • [ 01 ] == S
  • [ 1 <term1> <term2> ] == ( [<term1>] [<term2>] )

gdzie „ [...]” jest skrótem „znaczenia ...”. Tutaj Ki Ssą kombinatory KS- basis , i ( )jest operacją aplikacji logiki kombinatorycznej . (Przedrostek 1odpowiada lewemu nawiasowi, przy czym prawe nawiasy nie są potrzebne do uściślania).

Tak więc istnieją cztery równoważne sformułowania BCL, w zależności od sposobu kodowania trypletu (K, S, left parenthesis). Są to (00, 01, 1)(jak w obecnej wersji) (01, 00, 1), (10, 11, 0), i (11, 10, 0).

W semantyka operacyjne Bcl oprócz eta-redukcji (która nie jest wymagana dla Turingowi kompletności ) może być bardzo zwarty określony przez następujące przepisywania zasad subterms w danym okresie, podczas analizowania od lewej

  •  1100xy  → x
  • 11101xyz → 11xz1yz

gdzie x, yi zsą arbitralnymi podwarunkami. (Zauważ, na przykład, że ponieważ parsowanie odbywa się z lewej strony, 10000nie jest podkategorią 11010000.)

Jeden krok Reguły 110 automatów komórkowych w SK-Basis (napisany w języku Wolfram ).

BCL może być używany do replikowania algorytmów, takich jak maszyny Turinga i automaty komórkowe , BCL jest kompletnym systemem Turinga .

Zobacz też

Bibliografia

Dalsze lektury

  • Tromp, John (październik 2007). „Binarny rachunek lambda i logika kombinacyjna”. Losowość i złożoność, od Leibniza do Chaitina : 237–260. doi : 10.1142/9789812770837_0014 .

Zewnętrzne linki