TSP и TIP в системах λ-> и λP

Введение

Актуальность работы: задачи TSP и TIP теории типов имеют широкое распространение в области компьютерных наук и технологий, так как решение этих задач является важной частью при построении компиляторов.

В данной работе рассматриваются системы типов λ-> и λP, элементы которых включены в такие функциональные языки программирования, как Haskell и Idris (система типов которого включает зависимые типы).

Важной частью работы является использование элементов математической логики для рассмотрения систем типов λ-> и λP в виде логических выводов с помощью формул-типов.

Данные системы рассматриваются в следующих разделах математической логики:

• Prop – пропозициональная логика (нулевого порядка) для λ->;

• Pred – предикатная логика (первого порядка) для λP.

Цель работы: применение исчислений систем типов λ-> и λP для решения задач TSP и TIP и верификация полученных результатов с помощью компьютерных средств.

Предмет работы: задачи TSP и TIP в системах λ-> и λP.

Задачи теоретические и практические:

1. Грамматический разбор типизированных λ-термов (типов) по формальной грамматике псевдовыражений λ-куба Барендрегта.

2. Конструирование правил вывода для систем λ-> и λP с помощью правил

типизации λ-куба Барендрегта.

3. Вывод технологий решения задач TSP и TIP в системах λ-> и λP.

4. Решение задач TSP и TIP в системах λ-> и λP.

5. Перевод типов в формулы логических систем λ-> и λP, используя изоморфизм Карри-Говарда.

6. Верификация решений задач TSP и TIP в системах λ-> и λP. 

Заключение

В данной работе было проведено исследование, связанное с применением исчислений систем типов λ->и λP для решения задач TSP и TIP, а также верификация полученных результатов с помощью компьютерных средств.

Для достижения полученных результатов были решены следующие задачи:

1. Грамматический разбор типизированных λ-термов (типов) по формальной грамматике псевдовыражений λ-куба Барендрегта.

2. Конструирование правил вывода для систем λ-> и λP с помощью правил

типизации λ-куба Барендрегта.

3. Вывод технологий решения задач TSP и TIP в системах λ-> и λP.

4. Решение задач TSP и TIP в системах λ->и λP.

5. Перевод типов в формулы логических систем λ-> и λP, используя изоморфизм Карри-Говарда.

6. Верификация решений задач TSP и TIP в системах λ-> и λP.

К перспективам развития работы относится использование большего числа верификаторов – программ и языков программирования, которые позволили бы убедиться в правильности решения задач систем λ->и λP. Кроме того, важным вкладом в исследование может служить написание программы, автоматизирующей процесс решения задач теории типов для рассматриваемых в работе систем.