Знаймо

Додати знання

приховати рекламу

Цей текст може містити помилки.

Семантика обчислень



План:


Введення

Семантика обчислень - це визначення процесу обчислення у вигляді послідовності правил перезапису, яке разом з поданням про збіжність вперше були використані в контексті λ -Обчислення. Збіжність важлива також в системах автоматичного докази, заснованих на екваціональной логіці першого порядку.


1. Операційна семантика

Операційна семантика ( англ. operational semantics ) Використовується для синтаксичних понять мови. У ній функції розглядаються як текстуальні правильно побудовані визначення, що забезпечують застосування до аргументу, а не як функції в математичному розумінні цього терміна.

2. Денотаціонная семантика

Денотаціонная семантика ( англ. denotational semantics ) Виразами в програмі ставить у відповідність справжні математичні об'єкти. Найважливіші, у тому числі піонерські, результати побудови таких семантик отримані в роботах Д. Скотта (D. Scott), який першим побудував модель λ -Обчислення, засновану на уявленні про повне частково упорядкованому множині. Для цього їм були використані функції, безперервні на такій кількості.


3. Розвиток семантики

Предметом постійного інтересу і дослідження є побудова систем докази коректності, або правильності програм. Найбільш розробленими виявилися системи докази для випадку коректності функціональних програм, які сходять до системи LCF Робіна Мілнер і системі Р. Бойера (R. Boyer) і Дж. Мура (J. Moore).

Проведені в даний час дослідження зосереджені на побудові систем, заснованих на конструктивній логіці і встановлення аналогії між програмами і доказами. Істотно, що як програми, так і докази розглядаються зануреними в λ -Числення з типами, яке є формальною системою вищих порядків. Тим самим забезпечується можливість будувати тільки такі програми, які завершуються. Однією з подібних систем є система Coq.

В існуючих мовах використовуються різні підходи до побудови стратегії обчислення значення. У мовах сімейства ML, а також в Scheme застосовується обчислення за значенням у варіанті, допускає використання не обов'язково функціональних конструкцій. В інших мовах використовуються відкладені обчислення, які часто також називають лінивими обчисленнями. Механізми такого роду використані в мовах Miranda і Haskell.


Література

  • Вольфенгаген В. Е. Конструкції мов програмування. Прийоми опису. - М: АТ "Центр ЮрИнфоР", 2001. - 276 с. ISBN 5-89158-079-9

Цей текст може містити помилки.

Схожі роботи | скачати

Схожі роботи:
Модель обчислень
Модель обчислень
Зведення (теорія складності обчислень)
Семантика
Семантика Кріпке
Формальна семантика
Породжує семантика
Семантика (програмування)
Загальна семантика
© Усі права захищені
написати до нас
Рейтинг@Mail.ru