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

Содержание

Слайд 2

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

ПЛАН ЛЕКЦИИ

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

Слайд 3

НЕОБХОДИМОСТЬ ИЗУЧЕНИЯ ТЕОРЕТИЧЕСКИХ ОСНОВ ФП Базовые характеристики языков программирования (во многом

НЕОБХОДИМОСТЬ ИЗУЧЕНИЯ ТЕОРЕТИЧЕСКИХ ОСНОВ ФП

Базовые характеристики языков программирования (во многом определяются

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

ГРАММАТИКА ПСЕВДО-ЯЗЫКА t ::= {- термы: -} true {- константа «истина»

ГРАММАТИКА ПСЕВДО-ЯЗЫКА

t ::= {- термы: -}
true {- константа «истина» -}
false {-

константа «ложь» -}
if t then t else t {- условное выражение -}
0 {- константа «ноль» -}
succ t {- следующее число -}
pred t {- предыдущее число -}
iszero t {- проверка на ноль -}
Слайд 5

ОПРЕДЕЛЕНИЯ И ПОЯСНЕНИЯ Результаты вычислений 0 либо булевы константы, либо числа

ОПРЕДЕЛЕНИЯ И ПОЯСНЕНИЯ

Результаты вычислений 0 либо булевы константы, либо числа -

это все термы
Такие термы будем называть значениями

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

Слайд 6

ДРУГИЕ ОПРЕДЕЛЕНИЯ СИНТАКСИСА Определение 1 [термы через индукцию] Множество термов –

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

Определение 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 .
Слайд 7

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

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

Определение 2 [термы через правила вывода]: множество термов определяется

следующим образом
Слайд 8

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

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

 

Слайд 9

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

ДОМАШНЕЕ ЗАДАНИЕ:

Сколько элементов содержит S3?
Покажите ∀ i, Si⊆Si+1
Покажите, что S -

наименьшее множество
Слайд 10

T=S !! Для S должны выполняться условия 1. {true; false; 0}

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 .

Проверим!!!!

Слайд 11

T=S !! Пусть S’ удовлетворяет условиям наименьшего множества При помощи полной

T=S !!

Пусть S’ удовлетворяет условиям наименьшего множества
При помощи полной индукции

по i докажем что Si⊆S’
Для случая i=0
Для случая i=j+1>0, пусть Sj⊆S’

Докажем!!!

Слайд 12

ИНДУКЦИЯ НА ТЕРМАХ Из определения 1 если t ∈ T 1.

ИНДУКЦИЯ НА ТЕРМАХ

Из определения 1 если t ∈ T
1. t

является константой;
2. t результатом succ t1; pred t1; iszero t1 t13. t результатом if t1 then t2 else t3 t1, t2, t3
Слайд 13

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

ОПРЕДЕЛЕНИЯ

Определение 1

Слайд 14

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

ОПРЕДЕЛЕНИЯ

Определение 2

Слайд 15

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

ОПРЕДЕЛЕНИЯ

Определение 3

Слайд 16

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

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

Лемма 1

Слайд 17

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

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ

Индукция по глубине

Слайд 18

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

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ

Индукция по размеру

Слайд 19

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

ПРИНЦПЫ ИНДУКЦИИ ПО ТЕРМАМ

Структурная индукция

Слайд 20

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР) t ::= {- термы: -} true {-

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР)

t ::= {- термы: -}
true {- константа «истина»

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

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР) Множество термов – это наименьшее множество Τ

О СИНТАКСИСЕ ПСЕВДО-ЯЗЫКА (ПОВТОР)

Множество термов – это наименьшее множество Τ такое

, что
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 .

 

Слайд 22

СЕМАНТИЧЕСКИЕ СТИЛИ Для определения смысла программы необходим её математический эквивалент, а

СЕМАНТИЧЕСКИЕ СТИЛИ

Для определения смысла программы необходим её математический эквивалент, а для

его построения нам надо в точности знать свойства языка, на котором написана программа.
Проблема сводится к отысканию способа построения математических эквивалентов всех конструкций языка - к формализации его семантики.
Слайд 23

СЕМАНТИЧЕСКИЕ СТИЛИ Семантика языка — это смысловое значение слов. В программировании

СЕМАНТИЧЕСКИЕ СТИЛИ

Семантика языка — это смысловое значение слов. В программировании —

начальное смысловое значение операторов, основных конструкций языка и т. п.
1) i=0; while(i<5){i++;}
2) i=0; do{i++;}while(i<4);
Слайд 24

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

СЕМАНТИЧЕСКИЕ СТИЛИ

Различные подходы к формализации семантики:
Операционная семантика
Денотационая семантика
Аксиоматическая семантика
Интерпретационная семантика
Трансляционная семантика
Трансформационная

семантика
Слайд 25

СЕМАНТИЧЕСКИЕ СТИЛИ Операционная семантика Специфицирует поведение языка определяя простую абстрактную машину

СЕМАНТИЧЕСКИЕ СТИЛИ

Операционная семантика
Специфицирует поведение языка определяя простую абстрактную машину (использует термы

языка, а не машинные команды)
Состояние машины – терм
Поведение определяется функцией перехода.
Смысл терма t – конечное состояние
Слайд 26

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

СЕМАНТИЧЕСКИЕ СТИЛИ

Трансляционная семантика
Описание операционной семантики конструкций в терминах языков программирования высокого

уровня.
С помощью этого способа можно изучать язык, схожий с уже известным программисту.
Слайд 27

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

СЕМАНТИЧЕСКИЕ СТИЛИ

Трансформационная семантика
Описание операционной семантики конструкций языка в терминах этого

же языка. Трансформационная семантика является основой метапрограммирования.
Слайд 28

СЕМАНТИЧЕСКИЕ СТИЛИ Денотационная семантика Смысл терма - математические объекты (число, функция,

СЕМАНТИЧЕСКИЕ СТИЛИ

Денотационная семантика
Смысл терма - математические объекты (число, функция, их величины)
Построение

семантики:
нахождение набора семантических доменов (СД)
Определение функции интерпретации – (соответствие СД и термов)
Слайд 29

СЕМАНТИЧЕСКИЕ СТИЛИ Аксиоматическая семантика Семантика каждой синтаксической конструкции языка определяется как

СЕМАНТИЧЕСКИЕ СТИЛИ

Аксиоматическая семантика
Семантика каждой синтаксической конструкции языка определяется как некий набор

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

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

СЕМАНТИЧЕСКИЕ СТИЛИ

Интерпретационная семантика
описание операционной семантики конструкций в терминах языков программирования низкого

уровня (язык ассемблера, машинный код).
Позволяет выявлять медленно выполняемые участки программы, и зачастую используется в целях оптимизации кода программ.
Слайд 31

ВЫЧИСЛЕНИЯ

ВЫЧИСЛЕНИЯ

Слайд 32

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ) t → t’ понимается как t

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ)

t → t’ понимается как t за

1 шаг вычисляется как t’
Константы ни во что не вычисляются
E-IFTrue и E-IFFalse – рабочие правила
E-IF – правило соответствия
Определение: Экземпляр правила вывода получается при замене каждой метапеременной в заключении правила и во всех его предпосылках
Слайд 33

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

ВЫЧИСЛЕНИЯ

Пример

Слайд 34

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

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ)

Определение: Правило выполняется на отношении, если для

каждого экземпляра правила его заключение является элементом отношения, либо одна из его предпосылок не является таковой
Слайд 35

ВЫЧИСЛЕНИЯ (СЛУЧАЙ ТОЛЬКО БУЛЕВЫХ ВЫРАЖЕНИЙ) Определение: Одношаговое отношение вычисления → есть

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

бинарное отношение на термах, на котором выполняются все три правила
Если пара (t → t’) является элементом отношения вычисления, то говорят, что утверждение о вычислении t → t’ выводимо
Слайд 36

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

ВЫЧИСЛЕНИЯ

Пример

Слайд 37

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

ВЫЧИСЛЕНИЯ (СВОЙСТВА ОТНОШЕНИЯ ВЫЧИСЛЕНИЯ)

Теорема [теорема о детерминированности одношагового вычисления]

Слайд 38

ВЫЧИСЛЕНИЯ (СВОЙСТВА КОНЕЧНОГО СОСТОЯНИЯ) Результат вычисления – конечное состояние Определение 3

ВЫЧИСЛЕНИЯ (СВОЙСТВА КОНЕЧНОГО СОСТОЯНИЯ)

Результат вычисления – конечное состояние
Определение 3 Терм t

находится в нормальной форме если к нему не применимо никакое правило вычисления (∃t’, т.ч. t → t’ )
Теорема 2. Всякое значение находится в нормальной форме.
Теорема 3. Всякая нормальная форма есть значение
Слайд 39

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

ВЫЧИСЛЕНИЯ

Определение. Отношение многошагового вычисления →* это наименьшее отношение, т.ч.
(1) Если

t → t’, то t →* t’
(2) Для всех t выполняется t →* t
(3) Если t →* t’ и t’ →* t’’, то t →* t’’
Слайд 40

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

ВЫЧИСЛЕНИЯ

Теорема [теорема о единственности нормальных форм]
Если t →* u и t

→* u’ нормальные формы, то u=u’
Слайд 41

ВЫЧИСЛЕНИЯ Каждый терм можно вычислить и получить значение Теорема [завершение вычислений]

ВЫЧИСЛЕНИЯ

Каждый терм можно вычислить и получить значение
Теорема [завершение вычислений]
Для каждого терма

t существует нормальная форма t’ такая что и t →* t’
Слайд 42

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

ВЫЧИСЛЕНИЯ

Домашнее задание: упражнение 3.5.13, стр. 59

Слайд 43

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

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

Слайд 44

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

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

Определение. Терм если он находиться в нормальной форме, но

не является значением называется тупиковым термом
Пример: succ false
- Предыдущая
Сквер города Уфа «Четыре сезона»
Следующая -
Дескриптор. Построим деревянный дом вашей мечты под ключ за 3 месяца

Похожие презентации

Образование поверхностей и решение задач на пересечение поверхностей. (Лекция 4.2)
Правописание А – О в корнях ЛАГ – ЛОЖ, РАСТ – РОС. 5 КЛАСС. Урок нового материала. Учитель – Пахомова И.В.
Презентация Нефть
Цветы. Доставка
Надзор за сооружением. Организация и проведение осмотров соору­жений
Почему бухгалтерия должна быть похожа на Вконтакте?
Планирование аудиторской проверки
Менеджмент в туризме
Кадровая синхронизация
Субъекты информационного права Подготовил: Студент 3-го курса юридического факультета Сорокин А.А.
Кадровое агентство «ЭкспертПерсонал»
Вежливость и хорошие манеры
Что такое религия. Какие бывают религии
Auf den Spuren der Russlanddeutschen
Сегодня мы с вами рисуем пингвина - презентация для начальной школы_
Адаптивный спорт
Презентацию выполнила студентка – заочница 2 курса филологического ф – та Купчихина Елена Николаевна Владимир, 2013 год
Поиск информации по ДМ. Базы данных
Уголовно-правовая характеристика геноцида
5 КЛАСС
Финансовое прогнозирование
Лекция 5 Промежуточные товарные углеводородные продукты
Решения IZDAI24 для книгоиздателей
Срок жизни растений - презентация для начальной школы
Система творческих заданий в преподавании элективных курсов Глаголева Татьяна Васильевна
Театр ХХ века Экспрессионизм (Германия) Футуризм (Италия
Определение предпочтений потребителей блокаторов кальциевых каналов
Введение в морфологию латинского языка. Лекция №3
Вы можете прислать нам Вашу презентацию и мы опубликуем ее на сайте.
Обратная связь
Для правообладателей
Email: Нажмите что бы посмотреть