Кіріспе

Логикалық формализм айнымалылардың орнына комбинаторларды пайдалану арқылы

Комбинаторлық логика – математикалық логикада сандық айнымалылардың қажеттілігін жоюға арналған нотация. Оны Мозес Шёнфинкель мен Хаскелл Карри енгізді, ал соңғы кезде компьютер ғылымында есептеудің теориялық моделі ретінде, сондай-ақ функционалдық бағдарламалау тілдерін жобалау негізі ретінде қолданылды. Ол 1920 жылы Шёнфинкель енгізген комбинаторларға негізделген, функцияларды құрудың ұқсас тәсілін ұсыну және әсіресе предикат логикасында айнымалыларды атаудан толығымен бас тарту мақсатында жасалған. Комбинатор – жоғары реттік функция, ол тек функцияны қолдану және оның аргументтерінен нәтиже алу үшін бұрын анықталған комбинаторларды ғана пайдаланады.

Математикадан

Комбинациялық логика бастапқыда логикадағы сандық айнымалылардың рөлін түсіндіру үшін, негізінен оларды жою арқылы "алдын ала логика" ретінде ойластырылған. Сандық айнымалыларды жоюдың тағы бір тәсілі – Куиннің предикат функторы логикасы. Комбинациялық логиканың экспрессивті мүмкіндіктері әдетте бірінші реттік логикадан жоғары болса, предикат функторы логикасының экспрессивті мүмкіндіктері бірінші реттік логикамен сәйкес келеді (Куин 1960, 1966, 1976). Комбинациялық логиканың алғашқы авторы Мозес Шёнфинкель өзінің 1924 жылғы бастапқы мақаласынан кейін комбинациялық логика бойынша ештеңе жарияламады. Хаскелл Карри 1927 жылдың соңында Принстон университетінде оқытушы болып жұмыс істеген кезде комбинаторларды қайта ашты. 1930 жылдардың соңында Алонзо Черч және оның Принстондағы студенттері функционалдық абстракция үшін баламалы формализмді, яғни лямбда-есептеуін ойлап тапты, ол комбинациялық логикадан гөрі кеңінен танылды. Осы тарихи жағдайлардың салдарынан, теориялық информатика 1960 және 1970 жылдары комбинациялық логикаға қызығушылық танытқанға дейін, осы тақырыптағы барлық жұмыс Хаскелл Карри мен оның студенттері, немесе Бельгиядағы Роберт Фейс еңбектерімен байланысты болды. Curry and Feys (1958) және Curry және авторлар (1972) комбинациялық логиканың ерте тарихын қарастырады. Комбинациялық логика мен лямбда-есептеуді қазіргі заманғы тұрғысынан қарастыру үшін Барендрегттің кітабын қараңыз, онда 1960 және 1970 жылдары Дана Скотттың комбинациялық логика үшін жасаған модельдері талданған.

Есептеу саласында

Компьютерлік ғылымда комбинаторлық логика есептеудің жеңілдетілген моделі ретінде қолданылады, ол есептеу теориясы және дәлелдеу теориясында пайдаланылады. Қарапайымдылығына қарамастан, комбинаторлық логика есептеудің маңызды ерекшеліктерін қамтиды. Комбинаторлық логиканы лямбда-калькульдің бір түрі ретінде қарастыруға болады, онда лямбда-өрнектер (функционалды абстракцияны көрсететін) шектеулі комбинаторлар жиынтығымен алмастырылады, олар еркін айнымалылары жоқ бастапқы функциялар. Лямбда-өрнектерді комбинаторлық өрнектерге түрлендіру оңай, ал комбинаторлық редукция лямбда-редукциядан әлдеқайда қарапайым. Сондықтан комбинаторлық логика кейбір қатаң емес функционалдық бағдарламалау тілдерін және аппараттық құралдарды модельдеу үшін қолданылған. Бұл көзқарастың ең таза нысаны – Unlambda бағдарламалау тілі, оның жалғыз бастапқы элементтері S және K комбинаторлары, символдік кіріс/шығыспен толықтырылған. Практикалық бағдарламалау тілі болмаса да, Unlambda белгілі бір теориялық қызығушылық тудырады. Комбинаторлық логиканың әртүрлі интерпретациялары болуы мүмкін. Керридің көптеген алғашқы жұмыстары дәстүрлі логиканың аксиомалық жиынтықтарын комбинаторлық логика теңдеулеріне қалай аударуға болатынын көрсетті. Дана Скотт 1960-1970 жылдары модельдер теориясы мен комбинаторлық логиканы қалай біріктіруге болатынын көрсетті.

Комбинациялық есептеулер

Абстракция – бұл лямбда-есептеуде функцияларды жасаудың жалғыз тәсілі болғандықтан, комбинаторлық есептеуде оның орнын бірдеңе басуы керек. Абстракцияның орнына комбинаторлық есептеу басқа функцияларды құруға болатын бастапқы функциялардың шектеулі жиынтығын ұсынады.

CLK мен CLI арасындағы есептеу

Осы мақалада сипатталған CLK және CLI есептеулері арасында ажырату жасау қажет. Бұл айырмашылық λK және λI есептеулері арасындағы айырмашылыққа сәйкес келеді. λK есептеуінен өзгеше, λI есептеуі абстракцияларды былай шектейді: λx. E, мұнда x айнымалысы E-де кем дегенде бір рет еркін кездеседі. Осының салдарынан, комбинатор K λI есептеуінде де, CLI есептеуінде де кездеспейді. CLI тұрақтылары: I, B, C және S, олар барлық CLI терминдерін құруға мүмкіндік беретін негізді құрайды (теңдік бойынша). Кез келген λI терминін жоғарыда λK терминдерін CLK комбинаторларына түрлендіру үшін ұсынылған ережелерге ұқсас ережелер бойынша тең CLI комбинаторына түрлендіруге болады. Толық ақпарат үшін Барендрегтің (1984) 9-тарауын қараңыз.

Комбинаторлық есептеудің шешілмеуі

Нормалды форма – кез келген комбинаторлық термин, онда кездесетін бастапқы комбинаторлар, егер болса, оны одан әрі қысқарту үшін жеткілікті аргументтерге қолданылмайды. Кез келген комбинаторлық терминнің нормалды формасы бар ма, екі комбинаторлық термин эквивалентті ме сияқты мәселелер шешілмейді. Бұл lambda-терминдерге қатысты сәйкес мәселелер үшін ұқсас жолмен көрсетілуі мүмкін.

Функционалдық тілдерді құрастыру

Дэвид Тернер SASL бағдарламалау тілін іске асыру үшін өзінің комбинаторларын пайдаланды. Кеннет Иверсон APL-дің мұрагері J бағдарламалау тілінде Карри комбинаторларына негізделген бастауыш элементтерді қолданды. Бұл Иверсонның «жасырын бағдарламалау» деп атаған нәрсеге мүмкіндік берді, яғни айнымалылары жоқ функционалдық өрнектерде бағдарламалауға, сондай-шама айнымалылары жоқ бағдарламалармен жұмыс істеу үшін күшті құралдармен бірге. Кез келген APL сияқты тілде пайдаланушы анықтаған операторлармен жасырын бағдарламалау мүмкін екені белгілі болды.