Binarna logika kombinacyjna

Logika kombinatoryczna binarna ( BCL ) to język programowania komputerowego , który używa terminów binarnych 0 i 1 do stworzenia kompletnego sformułowania 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 boolowskiej. BCL ma zastosowanie w teorii złożoności wielkości programu ( złożoność Kołmogorowa ).

Definicja

Podstawa SK

Wykorzystując kombinatory K i S logiki kombinatorycznej , funkcje logiczne można przedstawić 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))
	I	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

Forma Backusa-Naura :

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

Semantyka

Semantykę denotacyjną BCL można określić w następujący sposób:

• [ 00 ] == K
• [ 01 ] == S
• [1 ] == ( [ ] [ ])

gdzie „ …” oznacza skrót „znaczenie … ”. Tutaj K i S są kombinatorami bazowymi KS , a ( ) jest działaniem aplikacji logiki kombinatorycznej . (Przedrostek 1 odpowiada lewemu nawiasowi, prawe nawiasy są niepotrzebne do ujednoznacznienia).

Istnieją więc cztery równoważne sformułowania BCL, w zależności od sposobu kodowania trójki (K, S, lewy nawias). Są to (00, 01, 1) (jak w obecnej wersji), (01, 00, 1) , (10, 11, 0) i (11, 10, 0) .

Semantykę operacyjną BCL, poza redukcją eta (która nie jest wymagana dla kompletności Turinga ), można bardzo zwięźle określić za pomocą następujących reguł przepisywania dla podwarunków danego terminu, analizując je od lewej:

• 1100xy → x
• 11101xyz → 11xz1yz

gdzie x , y i z są dowolnymi terminami podrzędnymi. (Zauważ na przykład, że ponieważ parsowanie odbywa się od lewej strony, 10000 nie jest podterminem 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 replikacji algorytmów, takich jak maszyny Turinga i automaty komórkowe , BCL jest kompletnym rozwiązaniem Turinga .

Zobacz też

• Jota i Jot

Dalsza lektura

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

Linki zewnętrzne

• John's Lambda Calculus i Combinatory Logic Playground
• Minimalna implementacja w C
• Brauner, Paweł. „Wykresy Lambda – lista odtwarzania YouTube” . YouTube . Zarchiwizowane od oryginału w dniu 2021-12-21.