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

Содержание слайда: Лекция 2. Тема 2. Бестиповые арифметические выражения Функциональное программирование

Содержание слайда: План лекции Термы. Синтаксис. Индукция на термах. Семантические стили.

Содержание слайда: Необходимость изучения теоретических основ ФП Базовые характеристики языков программирования (во многом определяются системой типов в ФП) Четкие, ясные, точные механизмы описания синтаксиса и семантики программ Пример: язык Haskell Поскольку Haskell представляет собой чисто функциональный язык, все вычисления осуществляются с помощью исчисления выражений (синтаксических термов), производящих значения (абстрактные сущности, которые мы рассматриваем как ответы). Каждое значение имеет связанный с ним тип (на интуитивном уровне мы можем рассматривать типы как множества значений). Налицо построенная строгая система типов закономерности и свойства которой необходимо учитывать, уметь формально обращаться с ней

Содержание слайда: Грамматика псевдо-языка t ::= {- термы: -} true {- константа «истина» -} false {- константа «ложь» -} if t then t else t {- условное выражение -} 0 {- константа «ноль» -} succ t {- следующее число -} pred t {- предыдущее число -} iszero t {- проверка на ноль -}

Содержание слайда: Определения и пояснения Результаты вычислений 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 [термы через правила вывода]: множество термов определяется следующим образом

Содержание слайда: Другие определения синтаксиса Определение 3 [термы через правила вывода]: множество термов определяется объединением множеств S= для каждого iN, где S0= Si+1= {true, false,0} {succ t1, pred t1, iszero t1  t1 Si} { if t1 then t2 else t3  t1, t2, t3 Si} T=S !!

Содержание слайда: Домашнее задание: Сколько элементов содержит 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<t; 3. t результатом if t1 then t2 else t3 t1, t2, t3 <t

Содержание слайда: Определения

Содержание слайда: Определения

Содержание слайда: Определения

Содержание слайда: Пример соотношения между числом констант в темме и его размером

Содержание слайда: Принцпы индукции по термам Индукция по глубине

Содержание слайда: Принцпы индукции по термам Индукция по размеру

Содержание слайда: Принцпы индукции по термам Структурная индукция

Содержание слайда: О синтаксисе псевдо-языка (повтор) 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

Содержание слайда: ВЫЧИСЛЕНИЯ Домашнее задание: упражнение 3.5.16-3.5.18, стр. 61,62 Кто УСПЕШНО выступит в понедельник – 5 дополнительных баллов на экзамене