Все шпоры по матлогике — часть 8
ОСОБЕННОСТИ:
1) Безтиповость: объекты могут являться функциями и аргументами, т. е. функции могут быть заданы программами (функции или процедуры Pascal), которые могут передаваться через формальные параметры другим программам.
2) исчисление представляет класс частичных функций – «
определимые функции», которые характеризуют неформальное понятие «эффективной вычислимости», тем самым связано с понятием «алгоритма вычисления».
3) исчисление является теоретической моделью современного функционального программирования (например, язык ЛИСП, который использует
исчисление в качестве промежуточного кода после 1-го этапа трансляции).
выражения и их вычисления.
Пример: . В
исчислении различают (устраняют различное понимание): символьную запись
и ее вызов (вычисление)
.
исчисление изучает функции и их аппликативное поведение (поведение относительно применения к аргументу). Выражение
можно считать как функцию от
(это записывается как
) и как функцию от
(это записывается как
). Вызовы могут быть следующими:
а) и
;
б)
в)
(30) Определение термов и
выражений
ОПРЕДЕЛЕНИЕ:
1. Каждая переменная или константа есть терм.
2. По любой переменной и любому
терму M строится новый
терм:
– функция от
, которую называют
абстракцией.
Замечание 1: Аналогичен в Pascal селектор записи «».
Замечание 2: Константы: целые числа, булевы константы, арифметические операции (функторы), булевы функции и т. п.
3. По любым термам M и N строится новый
терм MN, обозначающий применение (аппликацию) оператора M к аргументу N, то есть подстановка
позволяет получать
выражения (предикаты).
Замечание 3:Это определение термов (выражений) является правилом конструирования формул «по индукции».
Замечание 4: Правила вывода определяют алгоритм вычисления выражений
СВОРАЧИВАНИЕ,
СВОРАЧИВАНИЕ И РЕДУКЦИЯ
Определение 1: Константа, обозначающая функтор, применяемый к операндам, определяет подтерм, называемый редексом, а процесс применения называется
сворачиванием, в результате которого получается новое
выражение.
ПРИМЕР: То есть, «
» –
редекс,
сворачивание:
Определение 2: Терм вида называется
редексом.
Определение 3: Если редекс содержится в терме
и одно из его вхождений заменяется термом (подстановкой)
, то этот процесс
сворачивания (свертывания) обозначается
и означает, что терм
сворачивается к
выражению
.