tonitan / mscp-a Goto Github PK

Свершилось: удалось доказать нётеровость любой последовательности однозначных образцов относительно вложения их языков. В связи с чем, поскольку точного критерия однозначности образца пока нет, в качестве временной меры действуем через линал.

1. Разбиваем образец на фрагменты плоского разбиения
2. Строим матрицу кратностей параметров типа выражение во фрагментах и находим её ранг
   Если ранг этой матрицы совпадает с числом параметров, обобщение делать не надо.

Интересно будет поэкспериментировать ещё с построением сливающих подстановок. Возможно, этот приём окажется более полезен именно там.

Функция Type возвращает тип, подтип и свой аргумент, т.е. как минимум 2 терма. Здесь её результат сверяется с одиночным символом, так что условие здесь никогда не выполняется.

Если вчитаться в правые части выражений, то видно, что в них ошибки. В первом предложении функции Implode передаётся строка из цифр, в то время как имя должно начинаться на букву. Во втором предложении функции Symb передаётся литера, что приводит к ошибке отождествления.

Похоже, что код писался очень давно, когда ты только училась программировать на Рефале.

Лучше эти шесть строчек удалить.

Придумал хорошую задачу на верификацию.

В своём фреймворке переписал разбор целого числа с контролем переполнения:

https://github.com/Mazdaywik/refal-5-framework/blob/171a994a1e0070f098f267ec6e65ad4ea5b8a4ed/lib/R5FW-Parser.ref#L60-L62

https://github.com/Mazdaywik/refal-5-framework/blob/171a994a1e0070f098f267ec6e65ad4ea5b8a4ed/lib/R5FW-Parser.ref#L151-L186

Переписать решил из-за того, что Рефал-05 не умеет работать с длинной арифметикой.

Почему-то интерфейс GitHub не хочет раскрывать ссылки выше в листинг, поэтому приведу код:

DoScan {
  …

  t.Pos (s.Digit e.Line) e.Lines,
      <Type s.Digit>: 'D0' s.Digit =
    <DoScan-Number t.Pos t.Pos (s.Digit) (e.Line) e.Lines>;

  …
}

DoScan-Number {
  t.Pos t.Start (e.Number) (s.Next e.Line) e.Lines
    , <Type s.Next>: 'D0' s.Next
    = <DoScan-Number
        <IncCol t.Pos> t.Start (<DropZero e.Number> s.Next) (e.Line) e.Lines
      >;

  t.Pos t.Start (e.Number) (e.Line) e.Lines
    = <CheckNumber t.Start e.Number>
      <DoScan t.Pos (e.Line) e.Lines>;
}

DropZero {
  '0' = /* пусто */;
  e.Number = e.Number;
}

MAX-MACRODIGIT { = '4294967295' }

CheckNumber {
  t.Pos e.Number
    , <CheckNumber-Compare
        <Ord (<Lenw e.Number>) (<Lenw <MAX-MACRODIGIT>>)>
      >
    : {
        '+' = (TkError t.Pos 'Very big numeric literal: ' e.Number);

        s.Other = (TkMacroDigit t.Pos <Numb e.Number>);
      }
}

CheckNumber-Compare {
  () () = '0';
  (s.Eq e.X) (s.Eq e.Y) = <CheckNumber-Compare (e.X) (e.Y)>;
  (s.X e.X) (s.Y e.Y) = <Compare s.X s.Y>;
}

Здесь важно, что функция CheckNumber может проверять число, в котором нет лидирующих нулей, что функция DoScan-Number должна обеспечить:

DoScan {
  …

  t.Pos (s.Digit e.Line) e.Lines,
      <Type s.Digit>: 'D0' s.Digit =
    <DoScan-Number t.Pos t.Pos (s.Digit) (e.Line) e.Lines>;

  …
}

DoScan-Number {
  t.Pos t.Start (e.Number) (s.Next e.Line) e.Lines
    , <Type s.Next>: 'D0' s.Next
    = <DoScan-Number
        <IncCol t.Pos> t.Start (<DropZero e.Number> s.Next) (e.Line) e.Lines
      >;

  t.Pos t.Start (e.Number) (e.Line) e.Lines
    = <CheckNumber t.Start e.Number>
      <DoScan t.Pos (e.Line) e.Lines>;
}

DropZero {
  '0' = /* пусто */;
  e.Number = e.Number;
}

Обеспечивается это при помощи DropZero. В результате CheckNumber получит или литеру '0', или последовательность литер, которая на '0' не начинается.

Написал модель для MSCP-A:

$ENTRY Test {
  s.Digit e.Digits = <DoScan-Number (s.Digit) e.Digits>;
}

DoScan-Number {
  (e.Number) s.Next e.Line
    = <DoScan-Number
        (<DropZero e.Number> s.Next) e.Line
      >;

  (e.Number) (EOF) = <Check-NoLeadingZero e.Number>;
}

DropZero {
  '0' = /* пусто */;
  e.Number = e.Number;
}

Check-NoLeadingZero {
  '0' = Ok;
  '0' e.X = Fail;
  e.X = Ok;
}

К сожалению, MSCP-A не смог доказать, что лидирующие нули исключаются:

$ENTRY Go {
 s.z1 e.x1 =  <DoScan-Number_12_0 () s.z1 (e.x1)>;
}


DoScan-Number_12_0 {
 (e.x1) s.z1 (s.z2 e.x2) =  <DoScan-Number_12_0 (<Let_1 (e.x1) s.z1>) s.z2 (e.x2)>;
 () '0' ((EOF)) =  Ok;
 ('0' e.x1) s.z1 ((EOF)) =  Fail;
 (e.x1) s.z1 ((EOF)) =  Ok;
}


Let_1 {
 () '0' = ;
 (e.x1) s.z1 =  e.x1 s.z1;
}

/* This file is generated by MSCP at Tue Oct 18 16:52:03 2022.*/

/* Elapsed time of embeddings is 0.0.*/

/* Elapsed time of generalizations is 0.0.*/

Пробовал и другие варианты обеспечить инвариант — тоже не получилось:

• leading-zeros.zip

Вопросы:

• Можно ли как-то переписать тестовый пример, чтобы инвариант обеспечивался?
• Можно ли научить MSCP-A верифицировать эти примеры или выразительной силы рестрикций в уравнениях в словах тут недостаточно?