Кіріспе

Математикалық логика мен типтер теориясында λ кубі (сонымен қатар lambda кубі деп жазылады) – Хенк Барендрегттің конструкциялар есебінің жай типтелген λ есебінің жалпыламасы болып табылатын әртүрлі өлшемдерді зерттеу үшін ұсынған құрылымы. Кубтың әрбір өлшемі терминдер мен типтер арасындағы жаңа тәуелділік түріне сәйкес келеді. Мұндағы "тәуелділік" – термин немесе типтің басқа термин немесе типті байланыстыру қабілетін білдіреді. λ кубінің сәйкес өлшемдері: x ось: тәуелді типтерге сәйкес келетін, терминдерді байланыстыра алатын типтер. y ось: полиморфизмге сәйкес келетін, типтерді байланыстыратын терминдер. z ось: типтерді байланыстыра алатын типтер, (байлау) тип операторларына сәйкес келеді. Осы үш өлшемді әртүрлі жолдармен біріктіру кубтың 8 төбесін құрайды, олардың әрқайсысы әртүрлі типтегі жүйеге сәйкес келеді. λ кубі таза типтер жүйесі тұжырымдамасына жалпылауға болады.

(λ→) Ламбдалық есептеудің қарапайым түрі

λ кубындағы ең қарапайым жүйе – λ→ деп те аталатын қарапайым типтелген лямбда-есептеуі. Бұл жүйеде абстракцияны құрудың жалғыз жолы – бір терминнің екінші терминге тәуелді болуын қамтамасыз ету, оның типтеу ережесі:

(λω) Fω жүйесі

F жүйесінде басқа түрлерге тәуелді түрлерді беруге арналған құрылым енгізіледі. Бұл типтік конструктор деп аталады және "мәні ретінде түр бар функцияны" құруға мүмкіндік береді. Мұндай типтік конструктордың мысалы – берілген түрдегі деректермен белгіленген жапырақтары бар бинарлық ағаштардың түрі: , мұнда "" бейресми түрде " – түр" дегенді білдіреді. Бұл тип параметрін аргумент ретінде қабылдап, түрлі мәндердің түрін қайтаратын функция. Нақты бағдарламалауда бұл мүмкіндік оларды бастапқы элементтер ретінде қарастырмай, тілдің ішінде типтік конструкторларды анықтауға сәйкес келеді. Алдыңғы типтік конструктор OCaml-дегі белгіленген жапырақтары бар ағаштың келесі анықтамасына сәйкес келеді: type 'a tree = | Leaf of 'a | Node of 'a tree * 'a tree.

Бұл типтік конструкторды басқа түрлерге қолданып, жаңа түрлер алуға болады. Мысалы, бүтін сандар ағаштарының түрін алу үшін: type int tree = int tree.

F жүйесі көбінесе жеке қолданылмайды, бірақ типтік конструкторлардың тәуелсіз ерекшелігін бөліп көрсету үшін пайдалы.

(λP) Ламбда-П

λP жүйесінде, сондай-ақ ΛΠ деп аталатын және LF логикалық базасымен тығыз байланысты, тәуелді типтер болады. Бұл – мәндерге тәуелді болатын типтер. Жүйенің маңызды енгізу ережесі:

мұнда жарамды типтерді білдіреді. Жаңа тип құрастырушысы Кьюри-Говард изоморфизмі арқылы жалпы кванторға сәйкес келеді, ал λP жүйесі тұтастай алғанда тек импликация ғана жалғау ретінде қолданылатын бірінші реттік логикаға сәйкес келеді. Нақты бағдарламалаудағы осы тәуелді типтердің мысалы – белгілі бір ұзындықтағы векторлардың типі: ұзындығы – типке тәуелді мән.

(λω) Fω жүйесі

Fω жүйесі F жүйесінің конструкторын және F жүйесінен типтік конструкторларды біріктіреді. Осылайша, Fω жүйесі типтерге тәуелді мүшелерді де, типтерге тәуелді типтерді де қамтамасыз етеді.

λ2

λ2-де мұндай терминдерді If шарты арқылы алуға болады. Егер біздікін жалпы сандық белгі ретінде қарастырсақ, Кьюри-Ховард изоморфизмі арқылы бұл жарылыс принципінің дәлелі ретінде түсіндіріледі. Жалпы алғанда, λ2 өзін қоса алғанда, барлық типтер бойынша сандық белгіні қамтитын, яғни өз ішіндегі типтер бойынша сандық белгіні қамтитын импредикативті типтерді пайдалану мүмкіндігін қосады. Полиморфизм λ→-да құрастырылуы мүмкін емес функцияларды құруға да мүмкіндік береді. Нақтырақ айтқанда, λ2-де анықталатын функциялар екінші реттік Пеано арифметикасында толықтығы дәлелденген функциялар болып табылады. Атап айтқанда, барлық примитивті рекурсивті функциялар анықталады.

λP

λP-де терминдерге тәуелді типтерге ие болу мүмкіндігі логикалық предикаттарды өрнектеуге мүмкіндік береді. Мысалы, келесісі шығарылады: бұл Curry-Howard изоморфизмі арқылы, есептеу тұрғысынан қарағанда, тәуелді типтерге ие болу есептеу күшін арттырмайды, тек типтік қасиеттерді дәлірек өрнектеу мүмкіндігін ұсынады. Тәуелді типтермен жұмыс істегенде түрлендіру ережесі аса қажет, себебі ол типтегі терминдер бойынша есептеулер жасауға мүмкіндік береді. Мысалы, егер және болса, онда типін анықтау үшін түрлендіру ережесін қолдану қажет.

λω

λω-да келесі оператор анықталады, яғни, туынды λ2-де де қол жеткізіледі, бірақ полиморфты оператор тек ереже де болған жағдайда ғана анықтауға болады. Есептеу тұрғысынан алғанда, λω өте қуатты, және ол бағдарламалау тілдері үшін негіз ретінде қарастырылған.