Функциональное программирование. Бестиповые арифметические выражения. (Лекция 2.2)

ПЛАН ЛЕКЦИИ
Термы.
Синтаксис.
Индукция на термах.
Семантические стили.

НЕОБХОДИМОСТЬ ИЗУЧЕНИЯ ТЕОРЕТИЧЕСКИХ ОСНОВ ФП
Базовые характеристики языков программирования (во многом определяются системой типов в ФП)
Четкие, ясные, точные механизмы описания синтаксиса и семантики программ
Пример: язык Haskell
Поскольку Haskell представляет собой чисто функциональный язык,
все вычисления осуществляются с помощью исчисления выражений (синтаксических термов),
производящих значения (абстрактные сущности, которые мы рассматриваем как ответы).
Каждое значение имеет связанный с ним тип (на интуитивном уровне мы можем рассматривать типы как множества значений).
Налицо построенная строгая система типов закономерности и свойства которой необходимо учитывать, уметь формально обращаться с ней

ГРАММАТИКА ПСЕВДО-ЯЗЫКА
t ::= {- термы: -}
true {- константа «истина» -}
false {- константа «ложь» -}
if t then t else t {- условное выражение -}
0 {- константа «ноль» -}
succ t {- следующее число -}
pred t {- предыдущее число -}
iszero t {- проверка на ноль -}

ОПРЕДЕЛЕНИЯ И ПОЯСНЕНИЯ
Результаты вычислений 0 либо булевы константы, либо числа - это все термы
Такие термы будем называть значениями
t (c p до u)– метапеременная (служит для описания), служит заместителем какого-либо терма
Выражением будут называться любые синтактические объекты
Термы – выражения, которые представляют собой вычисления
Программа – терм, построенный на основе конструкций соответствующей приведенной грамматике
Числа - конструкции вида succ(succ(succ(0)))

ДРУГИЕ ОПРЕДЕЛЕНИЯ СИНТАКСИСА
Определение 1 [термы через индукцию]
Множество термов – это наименьшее множество Τ такое , что
1. {true; false; 0} „ ⊆ T ;
2. если t1 ∈ T , то {succ t1; pred t1; iszero t1} „ ⊆T ;
3. если t1 ∈ T , t2 ∈ T , t3 ∈ T , то if t1 then t2 else t3 ∈ T .

ДРУГИЕ ОПРЕДЕЛЕНИЯ СИНТАКСИСА
Определение 2 [термы через правила вывода]: множество термов определяется следующим образом

ДРУГИЕ ОПРЕДЕЛЕНИЯ СИНТАКСИСА

ДОМАШНЕЕ ЗАДАНИЕ:
Сколько элементов содержит S3?
Покажите ∀ i, Si⊆Si+1
Покажите, что S - наименьшее множество

T=S !!
Для S должны выполняться условия
1. {true; false; 0} „ ⊆ S ;
2. если t1 ∈ S , то {succ t1; pred t1; iszero t1} „ ⊆S ;
3. если t1 ∈ S , t2 ∈ S , t3 ∈ S , то if t1 then t2 else t3 ∈ S .
Проверим!!!!

T=S !!
Пусть S’ удовлетворяет условиям наименьшего множества
При помощи полной индукции по i докажем что Si⊆S’
Для случая i=0
Для случая i=j+1>0, пусть Sj⊆S’
Докажем!!!

ИНДУКЦИЯ НА ТЕРМАХ
Из определения 1 если t ∈ T
1. t является константой;
2. t результатом succ t1; pred t1; iszero t1 t1
3. t результатом if t1 then t2 else t3 t1, t2, t3

ОПРЕДЕЛЕНИЯ
Определение 1

ОПРЕДЕЛЕНИЯ
Определение 2

ОПРЕДЕЛЕНИЯ
Определение 3

ПРИМЕР СООТНОШЕНИЯ МЕЖДУ ЧИСЛОМ КОНСТАНТ В ТЕММЕ И ЕГО РАЗМЕРОМ
Лемма 1

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ
Индукция по глубине

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ
Индукция по размеру

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ
Структурная индукция

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР)
t ::= {- термы: -}
true {- константа «истина» -}
false {- константа «ложь» -}
if t then t else t {- условное выражение -}
0 {- константа «ноль» -}
succ t {- следующее число -}
pred t {- предыдущее число -}
iszero t {- проверка на ноль -}

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР)
Множество термов – это наименьшее множество Τ такое , что
1. {true; false; 0} „ ⊆ T ;
2. если t1 ∈ T , то {succ t1; pred t1; iszero t1} „ ⊆T ;
3. если t1 ∈ T , t2 ∈ T , t3 ∈ T , то if t1 then t2 else t3 ∈ T .

СЕМАНТИЧЕСКИЕ СТИЛИ
Для определения смысла программы необходим её математический эквивалент, а для его построения нам надо в точности знать свойства языка, на котором написана программа.
Проблема сводится к отысканию способа построения математических эквивалентов всех конструкций языка - к формализации его семантики.

СЕМАНТИЧЕСКИЕ СТИЛИ
Семантика языка — это смысловое значение слов. В программировании — начальное смысловое значение операторов, основных конструкций языка и т. п.
1) i=0; while(i<5){i++;}
2) i=0; do{i++;}while(i<4);

СЕМАНТИЧЕСКИЕ СТИЛИ
Различные подходы к формализации семантики:
Операционная семантика
Денотационая семантика
Аксиоматическая семантика
Интерпретационная семантика
Трансляционная семантика
Трансформационная семантика

СЕМАНТИЧЕСКИЕ СТИЛИ
Операционная семантика
Специфицирует поведение языка определяя простую абстрактную машину (использует термы языка, а не машинные команды)
Состояние машины – терм
Поведение определяется функцией перехода.
Смысл терма t – конечное состояние

СЕМАНТИЧЕСКИЕ СТИЛИ
Трансляционная семантика
Описание операционной семантики конструкций в терминах языков программирования высокого уровня.
С помощью этого способа можно изучать язык, схожий с уже известным программисту.

СЕМАНТИЧЕСКИЕ СТИЛИ
Трансформационная семантика
Описание операционной семантики конструкций языка в терминах этого же языка. Трансформационная семантика является основой метапрограммирования.

СЕМАНТИЧЕСКИЕ СТИЛИ
Денотационная семантика
Смысл терма - математические объекты (число, функция, их величины)
Построение семантики:
нахождение набора семантических доменов (СД)
Определение функции интерпретации – (соответствие СД и термов)

СЕМАНТИЧЕСКИЕ СТИЛИ
Аксиоматическая семантика
Семантика каждой синтаксической конструкции языка определяется как некий набор аксиом или правил вывода, который можно использовать для вывода результатов выполнения этой конструкции.
Чтобы понять смысл всей программы, эти аксиомы и правила вывода следует использовать так же, как при доказательстве обычных математических теорем.
Смысл терма, то что можно о нем доказать.
Когда программа выполнена, получаем доказательство - что вычисленные результаты удовлетворяют необходимым ограничениям на их значения относительно входных значений. То есть, доказано, что выходные данные представляют значения соответствующей функции, вычисленной по значениям входных данных.

СЕМАНТИЧЕСКИЕ СТИЛИ
Интерпретационная семантика
описание операционной семантики конструкций в терминах языков программирования низкого уровня (язык ассемблера, машинный код).
Позволяет выявлять медленно выполняемые участки программы, и зачастую используется в целях оптимизации кода программ.

ВЫЧИСЛЕНИЯ

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ)
t → t’ понимается как t за 1 шаг вычисляется как t’
Константы ни во что не вычисляются
E-IFTrue и E-IFFalse – рабочие правила
E-IF – правило соответствия
Определение: Экземпляр правила вывода получается при замене каждой метапеременной в заключении правила и во всех его предпосылках

ВЫЧИСЛЕНИЯ
Пример

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ)
Определение: Правило выполняется на отношении, если для каждого экземпляра правила его заключение является элементом отношения, либо одна из его предпосылок не является таковой

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ)
Определение: Одношаговое отношение вычисления → есть наименьшее бинарное отношение на термах, на котором выполняются все три правила
Если пара (t → t’) является элементом отношения вычисления, то говорят, что утверждение о вычислении t → t’ выводимо

ВЫЧИСЛЕНИЯ
Пример

ВЫЧИСЛЕНИЯ (СВОЙСТВА ОТНОШЕНИЯ ВЫЧИСЛЕНИЯ)
Теорема [теорема о детерминированности одношагового вычисления]

ВЫЧИСЛЕНИЯ (СВОЙСТВА КОНЕЧНОГО СОСТОЯНИЯ)
Результат вычисления – конечное состояние
Определение 3 Терм t находится в нормальной форме если к нему не применимо никакое правило вычисления (∃t’, т.ч. t → t’ )
Теорема 2. Всякое значение находится в нормальной форме.
Теорема 3. Всякая нормальная форма есть значение

ВЫЧИСЛЕНИЯ
Определение. Отношение многошагового вычисления →* это наименьшее отношение, т.ч.
(1) Если t → t’, то t →* t’
(2) Для всех t выполняется t →* t
(3) Если t →* t’ и t’ →* t’’, то t →* t’’

ВЫЧИСЛЕНИЯ
Теорема [теорема о единственности нормальных форм]
Если t →* u и t →* u’ нормальные формы, то u=u’

ВЫЧИСЛЕНИЯ
Каждый терм можно вычислить и получить значение
Теорема [завершение вычислений]
Для каждого терма t существует нормальная форма t’ такая что и t →* t’

ВЫЧИСЛЕНИЯ
Домашнее задание: упражнение 3.5.13, стр. 59

ВЫЧИСЛЕНИЯ (АРИФМЕТИЧЕСКИЕ ВЫРАЖЕНИЯ)

ВЫЧИСЛЕНИЯ (АРИФМЕТИЧЕСКИЕ ВЫРАЖЕНИЯ)
Определение. Терм если он находиться в нормальной форме, но не является значением называется тупиковым термом
Пример: succ false