Введение в теорию программирования. Функциональный подход

Функции SML для основных комбинаторов

Показывать лекцию целиком

Теоретические сведения

Согласно определению, комбинатором называется ламбда-выражение, не содержащее связанных переменных. Например, если в законе коммутативности

x+y = y+x

определить функцию

alpha(x,y) = x + y

и оператор С

(Cf)(x,y) = f(xy),

то данный закон примет следующий вид:

alpha = C alpha.

Формальная система комбинаторной логики естественным образом отображается на языки функционального программирования. В качестве иллюстрации определим SML-функции для базисных комбинаторов I, K, S:

fun Ix = x;
fun Kxy = x;
fun Sxyz = xz(yz);

Напомним, что характеристики перечисленных комбинаторных термов в рамках формальной системы комбинаторной логики имеют вид:

Ix = x,
Sxyz = xz(yz),
Kxy=x.

Задание

Сформулируйте формальную постановку задачи, запишите правила вывода и реализуйте программу на SML в соответствии с вариантом исполнения.

Варианты заданий

Выразить в базисе {K,S} комбинаторы с заданными характеристиками, убедиться в справедливости произведенных преобразований:

  • I, где Ia = a ;
  • B, где B abc = a(bc) ;
  • C, где C abc = acb ;
  • W, где W ab = abb ;
  • Y, где Y abcd = a(bc)(bd) ;
  • C[2], где C[2] abcd = acdb ;
  • C[2], где C[2] abcd = adbc ;
  • Y, где Ya = a (Ya) ;
  • C[3], где C[3] abcde = acdeb ;
  • C[3], где C[3] abcde = aebcd ;
  • B3, где B3 abcde = a(bcde) ;
  • F, где F abcd = a(bd)(cd) ;
    •

    Выразить в базисе {B,C,S} комбинаторы с заданными характеристиками, убедиться в справедливости произведенных преобразований:

  • I, где Ia = a ;
  • K, где K ab = a ;
  • S, где S abc = ac(bc) ;
  • W, где W ab = abb ;
  • Y, где Y abcd = a(bc)(bd) ;
  • C[2], где C[2] abcd = acdb ;
  • B2, где B2 abcd = a(bcd) ;
  • Y, где Ya = a (Ya) ;
  • C[3], где C[3] abcde = acdeb ;
  • C[3], где C[3] abcde = aebcd ;
  • F, где F abcd = a(bd)(cd).
    •
    Предыдущее занятие Следующее занятие
    Вернуться к учебному плану
    ^