Суперкомпиляция интерпретатора Лямбда-исчисления

Функции логики высказываний

index.htm - English text 

lambda.zip - архивированная директория. 

Используется пакет программ, доступный по адресам

Lambda calculus interpreter  ( http://drcjt.freeyellow.com/Lambda.html ) - головная страница,

Download the source code ( http://drcjt.freeyellow.com/lambda-1.00.tar.gz ) - пакет программ.

Пакет программ представлял собой аплет, поэтому головная программа Lambda.java была переделана.

Здесь мы рассматриваем суперкомпиляцию логических формул, записанных в Лямбда-терминологии. Фактически, получен компилятор логических Лямбда-формул в Ява-программы.

Суперкомпилируется метод test() в программе  lambda.java.

Специализация происходит по двум переменным:

• strStart - символьная константа, задающая логическую формулу,
• nVar - количество переменных в логической формуле.

Используются следующие логические операции: импликация, отрицание, конъюнкция и дизъюнкция. Их описание

    let true  = \x. \y. x
    let false = \x. \y. y
    let impl = \x. \y. x y true
    let not  = \x. x false true
    let or   = \x. \y. impl (not x) y
    let and  = \x. \y. not (or (not x) (not y))

Мы воспользовались тем свойством, что конъюнкция и дизъюнкция выражаются через  импликацию и  отрицание. 

Лямбда обозначается символом "\", в текстовых константах она раздваивается.

Остаточная программа вычисляет значение формулы для любого набора значений аргументов.

Перейдем с описанию 14 примеров. 

Все примеры оформлены по одному шаблону:

• Реализуемая логическая формула или заголовок примера.
• Значения strStart и nVar, по которым происходит специализация.
• Остаточная программа, откопированная из выходного файла суперкомпилятора вместе со строчками-комментариями, на первой из которых указано время суперкомпиляции до постпроцессинга, а на последней -- полное время."

Пример 1.      x & (y | z)

strStart = "\\x. \\y. \\z. and x (or y z)";
int nVar = 3;

//--------------------------------------  25 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]
	  && (param_18[1] || param_18[2])) {
	    return true;}
	  else {
	    return false;}
	}
//--------------------------------------  27 sec - JScp version 0.0.72 

Пример 2.      x | (y & z)

strStart = "\\x. \\y. \\z. or x (and y z)";
nVar = 3;

//--------------------------------------  24 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]
	  ||  param_18[1] && param_18[2]) {
	    return true;}
	  else {
	    return false;}
	}
//--------------------------------------  26 sec - JScp version 0.0.72 

Пример 3.      Implication

strStart = "\\x. \\y. impl x y";
nVar = 2;

//--------------------------------------   8 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]
	  && !param_18[1]) {
	    return false;}
	  else {
	    return true;}
	}
//--------------------------------------   9 sec - JScp version 0.0.72 

Пример 4.      Identically true function 

strStart = "\\x. \\y. impl x (impl y x)";
nVar = 2;

//--------------------------------------  10 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  return true;
	}
//--------------------------------------  10 sec - JScp version 0.0.72 

Пример 5.      Implication (3 variable)

strStart = "\\x. \\y. \\z. impl x y";
nVar = 3;

//--------------------------------------  17 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]
	  && !param_18[1]) {
	    return false;}
	  else {
	    return true;}
	}
//--------------------------------------  18 sec - JScp version 0.0.72 

Пример 6.      Identically true function

strStart = "\\x. \\y. \\z. impl x (impl y x)";
nVar = 3;

//--------------------------------------  20 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  return true;
	}
//--------------------------------------  21 sec - JScp version 0.0.72 

Пример 7.      Other identically true function

\\x. \\y. \\z. impl (impl x (impl y z)) (impl (impl x y) (impl x z))
nVar = 3;

//--------------------------------------  39 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  return true;
	}
//--------------------------------------  41 sec - JScp version 0.0.72 

Пример 8.      Implication (4 variable)

strStart = "\\x. \\y. \\z. \\u. impl x y";
nVar = 4;

//--------------------------------------  37 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]
	  && !param_18[1]) {
	    return false;}
	  else {
	    return true;}
	}
//--------------------------------------  39 sec - JScp version 0.0.72 

Пример 9.      True only in two cases

\\x. \\y. \\z. or (and x (and y z)) (and (not x) (and (not y) (not z)))
nVar = 3;

//--------------------------------------  59 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]) {
	    if (param_18[1]
	    &&  param_18[2]) {
	      return true;}
	    else {
	      return false;}}
	  else {
	    if (param_18[1]
	    ||  param_18[2]) {
	      return false;}
	    else {
	      return true;}}
	}
//--------------------------------------  65 sec - JScp version 0.0.72 

Пример 10.      (x & y) | (z & u)

strStart = "\\x. \\y. \\z. \\u. or (and x y ) (and z u)";
nVar = 4;

//--------------------------------------  75 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]) {
	    if (param_18[1]
	    ||  param_18[2] && param_18[3]) {
	      return true;}
	    else {
	      return false;}}
	  else {
	    if (param_18[2]
	    &&  param_18[3]) {
	      return true;}
	    else {
	      return false;}}
	}
//--------------------------------------  82 sec - JScp version 0.0.72 

Пример 11.      (x | not x) & (y | not y) & z = true & true & z = z

strStart = "\\x. \\y. \\z. and (and (or x (not x)) (or y (not y))) z";
nVar = 3;

//--------------------------------------  50 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[2]) {
	    return true;}
	  else {
	    return false;}
	}
//--------------------------------------  55 sec - JScp version 0.0.72 

Пример 12.      Max True - (x & y) | (y & z) | (x & z)

strStart = "\\x. \\y. \\z. or (and x y)  (or (and y z) (and x z))";
int nVar = 3;

//--------------------------------------  47 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]) {
	    if (param_18[1]
	    ||  param_18[2]) {
	      return true;}
	    else {
	      return false;}}
	  else {
	    if (param_18[1]
	    &&  param_18[2]) {
	      return true;}
	    else {
	      return false;}}
	}
//--------------------------------------  52 sec - JScp version 0.0.72 

Пример 13.      Mostik

\\x. \\y. \\z. \\u. \\v. 
    or (or (and x y) (and z u)) (or (and x (and v u)) (and z (and v y)))
nVar = 5;

//-------------------------------------- 340 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]) {
	    if (param_18[1]) {
	      return true;}
	    else {
	      if (param_18[2]) {
	        if (param_18[3]) {
	          return true;}
	        else {
	          return false;}}
	      else {
	        if (param_18[3]
	        &&  param_18[4]) {
	          return true;}
	        else {
	          return false;}}}}
	  else {
	    if (param_18[1]) {
	      if (param_18[2]
	      && (param_18[3] || param_18[4])) {
	        return true;}
	      else {
	        return false;}}
	    else {
	      if (param_18[2]
	      &&  param_18[3]) {
	        return true;}
	      else {
	        return false;}}}
	}
//-------------------------------------- 379 sec - JScp version 0.0.72 

Пример 14.      Equality

strStart = "\\x. \\y. and (impl x y) (impl y x)";
nVar = 2;

//--------------------------------------  14 sec - postprocessing...
	public static boolean test (final boolean[] param_18)
	{
	  if (param_18[0]) {
	    if (param_18[1]) {
	      return true;}
	    else {
	      return false;}}
	  else {
	    if (param_18[1]) {
	      return false;}
	    else {
	      return true;}}
	}
//--------------------------------------  16 sec - JScp version 0.0.72