Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

такой, что g(xi ,x2 ,...,x „,y )=0, т.е. при некоторых значениях xi,x2,...,x „ может и не существовать у такого, что g(Xj,X2,...,X „,y)=0. Очевидно, что всякая общерекурсивная функция является частично эекурсивной, но не наоборот. Можно доказать следующие важные теоремы. Теорема 5.11. Всякая частично рекурсивная функция (общерекурсивная) является частично вычислимой (вычислимой) по Маркову функцией Теорема 5.12. Всякая частично вычислимая (вычислимая) по Маркову функция, является частично рекурсивной (общерекурсивной). § 15. Ламбда-исчисление Прежде чем ввести ламбда-исчисление, укажем возможную область её использования в вычислительных моделях. Различают следующие вычислительные модели: императивную (процедурную) вычислительную модель (императив - повеление, требование), когда имеется последовательная система команд. Языки программирования, такие как АЛГОЛ, ФОРТРАН, С и т.п. основываются на этой вычислительной модели и объединяются под названием императивные или процедурные языки; логические вычислительные модели, основанные на вычислениях с помощью логики предикатов. Примеры таких языков Пролог, Дейталог, Параллельный Пролог; функциональные вычислительные модели, в которых программа рассматривается как множество определений функций. В основу этой модели положено так называемое «ламбда-исчисление». Примером языка, основанного на ламбда-исчислении, является язык ЛИСП; объектно-ориентированные вычислительные модели:, в императивных (процедурных) и функциональных вычислительных моделях операция принимается за субъект, а вычисления представляются в виде использования операций с некоторыми объектами. Однако если сделать наоборот, т.е. объект операции принять за субъект, а применение операций рассматривать как передачу запроса объекту, который и выполняет эту операцию, то такая модель является объектно-ориентированной, т.е. объекты рассматриваются как процессы. Реализованы в языках PLASMA, Mesa, LOOPS и др. Теперь перейдем к некоторым понятиям ламбда-исчисления. Ламбда-исчисление было введено Чёрчем как один из подходов для обоснования логики и математики. В дальнейшем часть этого исчисления явилась одной из теорий вычислений. 173