Binární kombinační logika - Binary combinatory logic

Binární kombinační logika (BCL) je formulací kombinační logika pouze pomocí symbolů 0 a 1.[1] BCL má aplikace v teorii složitosti velikosti programu (Kolmogorovova složitost ).[1][2]

Definice

Syntax

Backus – Naurova forma:

 <období> ::= 00 | 01 | 1 <období> <období>

Sémantika

The denotační sémantika BCL lze specifikovat takto:

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

kde "[...]"zkracuje" význam ...". Tady K. a S jsou KS- základní kombinátory, a ( ) je aplikace provoz, ze dne kombinační logika. (Předpona 1 odpovídá levé závorce, pravá závorka je pro disambiguaci zbytečná.)

Existují tedy čtyři ekvivalentní formulace BCL v závislosti na způsobu kódování tripletu (K, S, levá závorka). Tyto jsou (00, 01, 1) (jako v této verzi), (01, 00, 1), (10, 11, 0), a (11, 10, 0).

The operační sémantika BCL, kromě eta-redukce (pro kterou se nevyžaduje Turingova úplnost ), lze velmi kompaktně specifikovat následujícím textem přepis pravidla pro dílčí termíny daného termínu, analýza zleva:

  • 1100xy → x
  • 11101xyz → 11xz1yz

kde X, y, a z jsou libovolné podmnožiny. (Všimněte si například, že protože analýza probíhá zleva, 10000 není podmnožinou 11010000.)

Viz také

Reference

  1. ^ A b Tromp, John (2007), „Binární lambda kalkul a kombinační logika“, Náhodnost a složitost (PDF), World Sci. Publ., Hackensack, NJ, s. 237–260, CiteSeerX  10.1.1.695.3142, doi:10.1142/9789812770837_0014, ISBN  978-981-277-082-0, PAN  2427553.
  2. ^ Devine, Sean (2009), „Pohledy na algoritmickou entropii“, Entropie, 11 (1): 85–110, doi:10,3390 / e11010085, PAN  2534819

externí odkazy