Все шпоры по матлогике — часть 8

ОСОБЕННОСТИ:

1)  Безтиповость: объекты могут являться функциями и аргументами, т. е. функции могут быть заданы программами (функции или процедуры Pascal), которые могут передаваться через формальные параметры другим программам.

2)  исчисление представляет класс частичных функций – «определимые функции», которые характеризуют неформальное понятие «эффективной вычислимости», тем самым связано с понятием «алгоритма вычисления».

3)  исчисление является теоретической моделью современного функционального программирования (например, язык ЛИСП, который использует исчисление в качестве промежуточного кода после 1-го этапа трансляции).

выражения и их вычисления.

Пример: . В исчислении различают (устраняют различное понимание): символьную запись и ее вызов (вычисление) .

исчисление изучает функции и их аппликативное поведение (поведение относительно применения к аргументу). Выражение можно считать как функцию от (это записывается как ) и как функцию от (это записывается как ). Вызовы могут быть следующими:

а) и ;

б)

в)

(30) Определение термов и выражений

ОПРЕДЕЛЕНИЕ:

1.  Каждая переменная или константа есть терм.

2.  По любой переменной и любому терму M строится новый терм: – функция от , которую называют абстракцией.

Замечание 1: Аналогичен в Pascal селектор записи «».

Замечание 2: Константы: целые числа, булевы константы, арифметические операции (функторы), булевы функции и т. п.

3.  По любым термам M и N строится новый терм MN, обозначающий применение (аппликацию) оператора M к аргументу N, то есть подстановка позволяет получать выражения (предикаты).

Замечание 3:Это определение термов (выражений) является правилом конструирования формул «по индукции».

Замечание 4: Правила вывода определяют алгоритм вычисления выражений

СВОРАЧИВАНИЕ, СВОРАЧИВАНИЕ И РЕДУКЦИЯ

Определение 1: Константа, обозначающая функтор, применяемый к операндам, определяет подтерм, называемый редексом, а процесс применения называется сворачиванием, в результате которого получается новое выражение.

ПРИМЕР: То есть, «» – редекс, сворачивание:

Определение 2: Терм вида называется редексом.

Определение 3: Если редекс содержится в терме и одно из его вхождений заменяется термом (подстановкой) , то этот процесс сворачивания (свертывания) обозначается и означает, что терм сворачивается к выражению .