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