refal-5-lambda icon indicating copy to clipboard operation
refal-5-lambda copied to clipboard

Вопиющий случай распухания кода

Open Mazdaywik opened this issue 3 years ago • 16 comments

Проблема

При проверке pull request’а #361 упали автотесты: https://github.com/bmstu-iu9/refal-5-lambda/pull/361/checks?check_run_id=3404836202.

Из артефактов стало понятно, что не хватило лимита шагов на случайно сгенерированный тест:

2021-08-23T21:51:28.7711414Z Passing test-10_Mon-Aug-23-21-51-16-UTC-2021 (-OAS):
2021-08-23T21:51:39.5990547Z Passing test-10_Mon-Aug-23-21-51-16-UTC-2021 (-OADS):
2021-08-23T21:54:44.2696789Z TEST FAILED

Сам тест.

Данный тест удалось сузить до следующей программы (которой по-прежнему не хватает шагов):

$ENTRY Block {
  e.A t.B t.C X e.D
    , : e.X A e.Y e.D
    , :
    = ;

  e.X = e.X;
}

Скачать: bloat-condition.ref. Последнее условие в первом предложении пустое, и оно нужно. Без него ошибка не воспроизводится.

Я достал из лога программу с рассахаренными условиями (т.к. выпало на тесте без -OC+), упростил полученную программу, переименовал функции и переменные:

$ENTRY START {
  (e.A) t.B (e.C) = <Loop (e.A) t.B W S e.C>;
}

Loop {
  (e.Acc) e.Begin t.U t.V W e.End
    = <Loop (e.Acc e.Begin t.U) t.V W e.End>;

  (e.Acc) e.Rest = e.Acc e.Rest;
}

Скачать: bloat-basic.ref. Заметим, что функция Loop является синтаксическим мономом, если первое предложение убрать, её поведение сохранится.

Полный лог компиляции (11 мегабайт): bloat-basic.log.

Так вот, для функции Loop строится 56 экземпляров:

Фрагмент лога
Tue Aug 24 18:00:46 2021: History of START
    START@0: [(e.1) t.2 (e.3)]

Tue Aug 24 18:00:46 2021: History of Loop
    Loop@0: [(e.1) e.2]

Tue Aug 24 18:00:46 2021: History of Loop@1
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]

Tue Aug 24 18:00:46 2021: History of Loop@2
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]

Tue Aug 24 18:00:46 2021: History of Loop@3
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@4
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@4: [(e.0 t.1) t.2 W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@5
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]

Tue Aug 24 18:00:46 2021: History of Loop@6
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@7
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@8
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@8: [(e.0 t.1 t.2 s.3) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@9
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@4: [(e.0 t.1) t.2 W e.3]
    Loop@9: [(e.0 t.1 t.2) W W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@10
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@11
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@12
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@13
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@13: [(e.0 t.1 W t.2 W) t.3 W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@14
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@15
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@15: [(e.0 t.1 W s.2) t.3 W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@16
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@8: [(e.0 t.1 t.2 s.3) t.4 W e.5]
    Loop@16: [(e.0 t.1 t.2 s.3 t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@17
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]
    Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@18
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]

Tue Aug 24 18:00:46 2021: History of Loop@19
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@20
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@21
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@21: [(e.0 t.1 t.2 s.3 W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@22
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@13: [(e.0 t.1 W t.2 W) t.3 W e.4]
    Loop@22: [(e.0 t.1 W t.2 W t.3) W W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@23
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@23: [(e.0 t.1 t.2 t.3 t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@24
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@24: [(e.0 t.1 s.2 t.3 t.4 W W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@25
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@15: [(e.0 t.1 W s.2) t.3 W e.4]
    Loop@25: [(e.0 t.1 W s.2 t.3) W W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@26
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]
    Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]
    Loop@26: [(e.0 t.1 s.2 t.3) W W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@27
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]
    Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]
    Loop@27: [(e.0 t.1 s.2 s.3 t.4 W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@28
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]
    Loop@28: [(e.0 t.1 t.2 t.3) W W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@29
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]
    Loop@29: [(e.0 t.1 W t.2 W W) t.3 W e.4]

Tue Aug 24 18:00:46 2021: History of Loop@30
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@30: [(e.0 t.1 W s.2 t.3 W t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@31
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@31: [(e.0 t.1 t.2 s.3 t.4 W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@32
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@32: [(e.0 t.1 s.2 t.3 t.4 t.5) W W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@33
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@34
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@21: [(e.0 t.1 t.2 s.3 W) t.4 W e.5]
    Loop@34: [(e.0 t.1 t.2 s.3 W t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@35
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@21: [(e.0 t.1 t.2 s.3 W) t.4 W e.5]
    Loop@35: [(e.0 t.1 t.2 t.3 W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@36
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@13: [(e.0 t.1 W t.2 W) t.3 W e.4]
    Loop@22: [(e.0 t.1 W t.2 W t.3) W W e.4]
    Loop@36: [(e.0 t.1 t.2 t.3 t.4 t.5) W W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@37
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@23: [(e.0 t.1 t.2 t.3 t.4) W W e.5]
    Loop@37: [(e.0 t.1 t.2 t.3 t.4 W W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@38
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@24: [(e.0 t.1 s.2 t.3 t.4 W W) t.5 W e.6]
    Loop@38: [(e.0 t.1 t.2 t.3 t.4 t.5 W) t.6 W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@39
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]
    Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]
    Loop@26: [(e.0 t.1 s.2 t.3) W W e.4]
    Loop@39: [(e.0 t.1 s.2 t.3 W W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@40
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]
    Loop@28: [(e.0 t.1 t.2 t.3) W W e.4]
    Loop@40: [(e.0 t.1 t.2 t.3 W W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@41
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]
    Loop@29: [(e.0 t.1 W t.2 W W) t.3 W e.4]
    Loop@41: [(e.0 t.1 W t.2 t.3 W) t.4 W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@42
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@30: [(e.0 t.1 W s.2 t.3 W t.4) W W e.5]
    Loop@42: [(e.0 t.1 s.2 t.3 t.4 t.5 t.6) W W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@43
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@31: [(e.0 t.1 t.2 s.3 t.4 W) t.5 W e.6]
    Loop@43: [(e.0 t.1 t.2 s.3 t.4 W t.5) W W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@44
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@32: [(e.0 t.1 s.2 t.3 t.4 t.5) W W e.6]
    Loop@44: [(e.0 t.1 s.2 t.3 t.4 t.5 W W) t.6 W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@45
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]
    Loop@45: [(e.0 t.1 t.2 s.3 t.4 t.5) W W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@46
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]
    Loop@46: [(e.0 t.1 t.2 t.3 t.4 t.5 t.6 W) t.7 W e.8]

Tue Aug 24 18:00:46 2021: History of Loop@47
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@21: [(e.0 t.1 t.2 s.3 W) t.4 W e.5]
    Loop@35: [(e.0 t.1 t.2 t.3 W) t.4 W e.5]
    Loop@47: [(e.0 t.1 t.2 t.3 W t.4) W W e.5]

Tue Aug 24 18:00:46 2021: History of Loop@48
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@13: [(e.0 t.1 W t.2 W) t.3 W e.4]
    Loop@22: [(e.0 t.1 W t.2 W t.3) W W e.4]
    Loop@36: [(e.0 t.1 t.2 t.3 t.4 t.5) W W e.6]
    Loop@48: [(e.0 t.1 t.2 t.3 t.4 t.5 W W) t.6 W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@49
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@24: [(e.0 t.1 s.2 t.3 t.4 W W) t.5 W e.6]
    Loop@38: [(e.0 t.1 t.2 t.3 t.4 t.5 W) t.6 W e.7]
    Loop@49: [(e.0 t.1 t.2 t.3 t.4 t.5 W t.6) W W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@50
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]
    Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]
    Loop@26: [(e.0 t.1 s.2 t.3) W W e.4]
    Loop@39: [(e.0 t.1 s.2 t.3 W W) t.4 W e.5]
    Loop@50: [(e.0 t.1 s.2 t.3 t.4 W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@51
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@18: [(e.0 t.1 W t.2) W W e.3]
    Loop@28: [(e.0 t.1 t.2 t.3) W W e.4]
    Loop@40: [(e.0 t.1 t.2 t.3 W W) t.4 W e.5]
    Loop@51: [(e.0 t.1 t.2 t.3 t.4 W) t.5 W e.6]

Tue Aug 24 18:00:46 2021: History of Loop@52
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@30: [(e.0 t.1 W s.2 t.3 W t.4) W W e.5]
    Loop@42: [(e.0 t.1 s.2 t.3 t.4 t.5 t.6) W W e.7]
    Loop@52: [(e.0 t.1 t.2 t.3 t.4 t.5 t.6) W W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@53
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@5: [(e.0 t.1 W S) W W e.2]
    Loop@11: [(e.0 t.1 W S W W) t.2 W e.3]
    Loop@19: [(e.0 t.1 W s.2 t.3 W) t.4 W e.5]
    Loop@30: [(e.0 t.1 W s.2 t.3 W t.4) W W e.5]
    Loop@42: [(e.0 t.1 s.2 t.3 t.4 t.5 t.6) W W e.7]
    Loop@53: [(e.0 t.1 s.2 t.3 t.4 t.5 t.6 W W) t.7 W e.8]

Tue Aug 24 18:00:46 2021: History of Loop@54
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]
    Loop@45: [(e.0 t.1 t.2 s.3 t.4 t.5) W W e.6]
    Loop@54: [(e.0 t.1 t.2 s.3 t.4 t.5 W W) t.6 W e.7]

Tue Aug 24 18:00:46 2021: History of Loop@55
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@12: [(e.0 t.1 W S W t.2) W W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]
    Loop@46: [(e.0 t.1 t.2 t.3 t.4 t.5 t.6 W) t.7 W e.8]
    Loop@55: [(e.0 t.1 t.2 t.3 t.4 t.5 t.6 W t.7) W W e.8]

Tue Aug 24 18:00:46 2021: History of Loop@56
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@3: [(e.0 t.1 W S) t.2 W e.3]
    Loop@7: [(e.0 t.1 W S t.2) W W e.3]
    Loop@14: [(e.0 t.1 s.2 t.3 t.4) W W e.5]
    Loop@24: [(e.0 t.1 s.2 t.3 t.4 W W) t.5 W e.6]
    Loop@38: [(e.0 t.1 t.2 t.3 t.4 t.5 W) t.6 W e.7]
    Loop@49: [(e.0 t.1 t.2 t.3 t.4 t.5 W t.6) W W e.7]
    Loop@56: [(e.0 t.1 t.2 t.3 t.4 t.5 t.6 t.7) W W e.8]

Остаточная программа до прогонки экземпляров содержит 835 строк, после прогонки экземпляров — 15 555 строк (да, четыре пятёрки: residual.txt).

Типичный экземпляр до прогонки экземпляров:

  Loop@32 {
    (e.X1) t.X3 s.X2 t.X4 t.X5 t.X6 W e.X4
      = <Loop@36 (e.X1 t.X3) s.X2 t.X4 t.X5 t.X6 W e.X4>;

    (e.X1) t.X3 s.X2 t.X4 t.X5 t.X6 t.X7 W e.X5
      = <Loop@44 (e.X1) t.X3 s.X2 t.X4 t.X5 t.X6 t.X7 e.X5>;

    (e.X1) t.X3 s.X2 t.X4 t.X5 t.X6 e.X4 t.X7 t.X8 W e.X8
      = <Loop@4 (e.X1 t.X3 s.X2 t.X4 t.X5 t.X6 W W e.X4) t.X7 t.X8 e.X8>;

    (e.X1) t.X3 s.X2 t.X4 t.X5 t.X6 e.X3
      = e.X1 t.X3 s.X2 t.X4 t.X5 t.X6 W W e.X3;
  }

Начало финальной остаточной программы:

  $ENTRY START;

  START {
    (e.A) t.B (W W W W W e.C5) = <Loop@10 (e.A t.B W S) W W W e.C5>;

    (e.A) t.B (W W W W t.C4 W W e.C7)
      = <Loop@26 (e.A t.B W S W W) W W t.C4 e.C7>;

    (e.A) t.B (W W W W t.C4 W t.C6 W W e.C9)
      = <Loop@26 (e.A t.B W S W W W W) t.C4 W t.C6 e.C9>;

    (e.A) t.B (W W W W t.C4 W t.C6 W t.C8 W e.C10)
      = <Loop@31 (e.A t.B W S W W W) W t.C4 W t.C6 t.C8 e.C10>;

    (e.A) t.B (W W W W t.C4 W t.C6 W e.C8)
      = <Loop@27*2 (e.A t.B W S W) W W W t.C4 t.C6 e.C8>;

    (e.A) t.B (W W W W t.C4 W e.C6) = <Loop@17*2 (e.A t.B W) S W W t.C4 e.C6>;

    (e.A) t.B (W W W W e.C4) = <Loop@10*2 (e.A t.B W) S W W e.C4>;

    (e.A) t.B (W W W t.C3 W W e.C6) = <Loop@26 (e.A t.B W S W) W W t.C3 e.C6>;

    (e.A) t.B (W W W t.C3 W t.C5 W W e.C8)
      = <Loop@26 (e.A t.B W S W W W) t.C3 W t.C5 e.C8>;

    (e.A) t.B (W W W t.C3 W t.C5 W t.C7 W e.C9)
      = <Loop@31 (e.A t.B W S W W) W t.C3 W t.C5 t.C7 e.C9>;

    (e.A) t.B (W W W t.C3 W t.C5 W e.C7)
      = <Loop@27*2 (e.A t.B W S) W W W t.C3 t.C5 e.C7>;

    (e.A) t.B (W W W t.C3 W e.C5) = <Loop@17*2 (e.A t.B) W S W t.C3 e.C5>;

    (e.A) t.B (W W W e.C3) = <Loop@10*2 (e.A t.B) W S W e.C3>;

    (e.A) t.B (W W t.C2 W W e.C5) = <Loop@18 (e.A t.B W S) W t.C2 e.C5>;

    (e.A) t.B (W W t.C2 W t.C4 W W W W W W e.C11)
      = <Loop@52 (e.A t.B W S W W t.C2) W t.C4 W W W W e.C11>;

…

Почему вопиющий случай? Зачем новая заявка (почему не #332)?

Вопиющая потому что

  • во-первых, 11 строк кода взрываются до 835/15 555, что, очевидно, жесть,
  • во-вторых, я уже хотел выпустить версию 3.4, как вылезла эта ошибка.

Заявка #332 предполагается как долгоиграющая — когда я её буду исправлять, не известно. А эту хочется исправить в самое ближайшее время.

Возможные решения

Забить

Т.е. запушить новый коммит (он должен быть с обновлением NEWS.md, и, если повезёт, в случайных тестах эта ошибка не повторится.

  • ✔Самое простое решение.
  • ❌Ошибку всё равно придётся решать.
  • ❌Не красиво, что ошибка сборки в #361 не исправлена (другие ошибки сборки исправлялись последующими коммитами).

Придумать костыль

Например, снизить наибольшее число экземпляров (сейчас такой костыль есть, ограничивает число экземпляров 99, 54c28cad9). Либо можно ограничить максимальную глубину истории. Для последнего можно самоприменить компилятор и посмотреть максимальную глубину истории в нём.

  • ✔Относительно простое решение.
  • ❌Костыль всегда не эстетичен. Грязное решение.

Ослабить отношение остановки

Сейчас используется честное отношение Хигмана-Крускала. Выбор другого варианта — это всё-таки исследовательская работа, быстро сделать не получится. Идеи описаны в комментариях https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-808697324, https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-815664005 и https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-883934769.

  • ✔Возможно, заработает.
  • ❌Другое отношение снизит глубину оптимизации. Возможно, снизит криво — очевидные оптимизируемые места оптимизироваться не будут. Т.е. надо внимательно исследовать.
  • ❌Хз, какое новое отношение выбрать.

Специальное сопоставление с образцом для специализации

Описано оно в комментарии https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-890483185. Если кратко, то алгоритм сопоставления с образцом, злоупотребляя динамическим обобщением, гарантирует, что для любого предложения специализируемой функции построится не более одного предложения в экземпляре. Участки аргумента, сопоставление с которыми приводит к ветвлению, принудительно обобщаются.

  • ✔Скорее всего, решит описываемую проблему. В экземплярах сейчас строится по 4 предложения, т.е. первое предложение расщепляется на 3. Применение нового алгоритма сопоставления с образцом приведёт, скорее всего, к динамическому обобщению до тривиальной сигнатуры.
  • ✔Возможно, можно будет отказаться от явного обобщения участков вида e.X … e.Y, описанных в том же комментарии https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-890483185 и реализованных в фиксации 916efbf.
  • ❌Нетривиальная правка алгоритма обобщённого сопоставления. В состояние алгоритма нужно будет протащить флаг, указывающий на специальный режим работы.
  • ❌Нужно проверить, насколько ухудшится в этом режиме оптимизация.

Перестройка сверху (честная)

В комментарии https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-901267648 предлагается серьёзно модифицировать алгоритм оптимизации, чтобы при специализации использовалась перестройка сверху. Скорее всего, это снизит число экземпляров в данной задаче до разумной величины (см. первый комментарий https://github.com/bmstu-iu9/refal-5-lambda/issues/362#issuecomment-904865271).

  • ✔Скорее всего, это решит проблему. По историям сигнатур видно, что в некоторых случаях перестройка сверху срезала бы часть истории:
      START@0: [(e.1) t.2 (e.3)]
      Loop@1: [(e.0) t.1 W S e.2]
      Loop@2: [(e.0 t.1 W) S W e.2]
      Loop@5: [(e.0 t.1 W S) W W e.2]
      Loop@10: [(e.0 t.1 s.2 s.3) W W e.4]  ← здесь
      Loop@17: [(e.0 t.1 s.2 s.3 W W) t.4 W e.5]
      Loop@26: [(e.0 t.1 s.2 t.3) W W e.4]  ← и здесь
      Loop@39: [(e.0 t.1 s.2 t.3 W W) t.4 W e.5]
      Loop@50: [(e.0 t.1 s.2 t.3 t.4 W) t.5 W e.6]
    
    Экземпляры Loop@10 и Loop@26 различаются только s- и t-переменными:
    Loop@10 {
      (e.X) t.X s.X s.X1 W e.X2 = <Loop@10 (e.X t.X) s.X s.X1 W e.X2>;
    
      (e.X) t.X s.X s.X1 t.X1 W e.X3 = <Loop@17 (e.X) t.X s.X s.X1 t.X1 e.X3>;
    
      (e.X) t.X s.X s.X1 e.X2 t.X3 t.X4 W e.X6
        = <Loop@4 (e.X t.X s.X s.X1 W W e.X2) t.X3 t.X4 e.X6>;
    
      (e.X) t.X s.X s.X1 e.X1 = e.X t.X s.X s.X1 W W e.X1;
    }
    
    Loop@26 {
      (e.X1) t.X2 s.X2 t.X3 W e.X3 = <Loop@28 (e.X1 t.X2) s.X2 t.X3 W e.X3>;
    
      (e.X1) t.X2 s.X2 t.X3 t.X4 W e.X5
        = <Loop@39 (e.X1) t.X2 s.X2 t.X3 t.X4 e.X5>;
    
      (e.X1) t.X2 s.X2 t.X3 e.X3 t.X5 t.X6 W e.X8
        = <Loop@4 (e.X1 t.X2 s.X2 t.X3 W W e.X3) t.X5 t.X6 e.X8>;
    
      (e.X1) t.X2 s.X2 t.X3 e.X2 = e.X1 t.X2 s.X2 t.X3 W W e.X2;
    }
    
  • ✔Это довольно общее решение.
  • ❌Громоздкие переделки архитектуры оптимизатора, для быстрого патча не подходит.

Перестройка сверху (халтурная)

Сейчас при обнаружении зацикливания между старой сигнатурой F@i и новой сигнатурой F@j вычисляется их обобщение, назовём его F@k = MSG(F@i, F@j). Если F@k ≡ F@i, то это обычное зацикливание, вызываем ранее построенный экземпляр. Если нет, то вызывается и строится экземпляр для обобщённой сигнатуры F@k. История экземпляра F@k растёт от истории F@j. Это перестройка снизу.

Предлагается сделать почти грязный хак. А именно, при срабатывании условия остановки в случае F@k = MSG(F@i, F@j) ≠ F@i строить не только экземпляр F@k, как и раньше, но ещё и патчить старый экземпляр F@i, заменяя всё его тело на единственный вызов F@k:

F@i {
  ARG = <F@k ARG′>
}

История экземпляра F@k будет расти не от истории F@j, а от F@i. Назовём это халтурной перестройкой сверху.

Очевидно, что экземпляры, построенные после F@i, в программе останутся, хоть вызываться из F@i не будут. Возможно, специализатор продолжит оптимизировать в них заведомо бессмысленные вызовы. Они могут потом потереться на последнем проходе — удалении невызываемых функций¹. Или не потереться, если в них есть «косые стрелки».

¹ Этот проход в качестве корневого множества рассматривает все функции без суффиксов — функции исходной программы. Поэтому в логе можно видеть функцию Loop, которая ниоткуда не вызывается.

Пропатченные экземпляры вида F@i из примера выше будут встраиваться в точки вызова на проходе прогонки экземпляров.

Если специализация разных дочерних экземпляров будет требовать разный патч для родителя, то будет выбираться произвольный патч — какой первый попадётся.

  • ✔Подход будет снижать объём остаточной программы как минимум из-за того, что размер некоторых экземпляров будет сокращаться (тем более, они в режиме -OA будут встраиваться в точки вызова, а затем вытираться как неиспользуемые).
  • ✔Вероятно, решит и текущую задачу. Выход за лимит шагов возникал вроде на стадии прогонки экземпляров.
  • ✔❓Думаю, проблему можно решить не более чем 100 новыми строками кода. Серьёзно сломаться ничего не должно.

Вывод

А нет пока вывода. Я ещё не выбрал вариант. Напишу в комментариях. Склоняюсь к последнему.

@TonitaN, какой вариант тебе больше нравится?

Mazdaywik avatar Aug 24 '21 18:08 Mazdaywik

Данный пример содержит открытые e-переменные. Есть другой суперкомпилятор (помимо кривого ограниченного оптимизатора в Рефале-5λ), который умеет обрабатывать программы с открытыми e-переменными — MSCP-A. Интересно посмотреть на нём этот пример.

Версия суперкомпилятора — последний коммит https://github.com/TonitaN/MSCP-A/commit/bf4a5175549ff913c52a68f5270a3370d3bf9daa на момент написания этого комментария.

Пример

$ENTRY START {
  (e.A) t.B (e.C) = <Loop (e.A) t.B W S e.C>;
}

Loop {
  (e.Acc) e.Begin t.U t.V W e.End
    = <Loop (e.Acc e.Begin t.U) t.V W e.End>;

  (e.Acc) e.Rest = e.Acc e.Rest;
}

успешно отсуперкомпилировался, получилась такая программа:

Остаточная программа


$ENTRY Go {
 (e.x1) t.y1 (e.x2) =  <InputFormat_0 (e.x1) t.y1 (e.x2)>;
}


InputFormat_0 {
 (e.x1) t.y1 (W W e.x2) =  <Loop_12_0 (e.x1) t.y1 () (e.x2)>;
 (e.x1) t.y1 (W t.y2 W e.x2) =  <Loop_12_4 (e.x1) t.y1 () t.y2 (e.x2)>;
 (e.x1) t.y1 (W e.x2 t.y2 t.y3 W e.x3) =  <Loop_12_6 (e.x1) t.y1 (e.x2) t.y2 () t.y3 (e.x3)>;
 (e.x1) t.y1 (W e.x2) =  e.x1 t.y1 W S W e.x2;
 (e.x1) t.y1 (t.y2 W e.x2) =  <Loop_12_8 (e.x1) t.y1 () t.y2 (e.x2)>;
 (e.x1) t.y1 (e.x2 t.y2 t.y3 W e.x3) =  <Loop_12_10 (e.x1) t.y1 (e.x2) t.y2 () t.y3 (e.x3)>;
 (e.x1) t.y1 (e.x2) =  e.x1 t.y1 W S e.x2;
}


Loop_12_0 {
 (e.x1) t.y1 (e.x2) (W e.x3) =  <Loop_12_0 (e.x1) t.y1 (e.x2 W) (e.x3)>;
 (e.x1) t.y1 (e.x2) (t.y2 W e.x3) =  <Loop_12_1 (e.x1) t.y1 (e.x2) () t.y2 (e.x3)>;
 (e.x1) t.y1 (e.x2) (e.x3 t.y2 t.y3 W e.x4) =  <Loop_12_2 (e.x1) t.y1 (e.x2) (e.x3) t.y2 () t.y3 (e.x4)>;
 (e.x1) t.y1 (e.x2) (e.x3) =  e.x1 t.y1 W S e.x2 W W e.x3;
}


Loop_12_1 {
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (W e.x4) =  <Loop_12_0 (e.x1) t.y1 (e.x2 W W e.x3 t.y2) (e.x4)>;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (t.y3 W e.x4) =  <Loop_12_1 (e.x1) t.y1 (e.x2) (e.x3 t.y2 W) t.y3 (e.x4)>;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4 t.y3 t.y4 W e.x5) =  <Loop_12_1 (e.x1) t.y1 (e.x2)
                                                              (e.x3 t.y2 W e.x4 t.y3) t.y4 (e.x5)
                                                           >;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4) =  e.x1 t.y1 W S e.x2 W W e.x3 t.y2 W e.x4;
}


Loop_12_2 {
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4) t.y3 (W e.x5) =  <Loop_12_0 (e.x1) t.y1
                                                           (e.x2 W W e.x3 t.y2 e.x4 t.y3) (e.x5)
                                                        >;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4) t.y3 (t.y4 W e.x5) =  <Loop_12_2 (e.x1) t.y1 (e.x2) (e.x3)
                                                                t.y2 (e.x4 t.y3 W) t.y4 (e.x5)
                                                             >;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4) t.y3 (e.x5 t.y4 t.y5 W e.x6) =  <Loop_12_2 (e.x1) t.y1 (e.x2) (e.x3)
                                                                          t.y2 (e.x4 t.y3 W e.x5 t.y4) t.y5
                (e.x6)
                                                                       >;
 (e.x1) t.y1 (e.x2) (e.x3) t.y2 (e.x4) t.y3 (e.x5) =  e.x1 t.y1 W S e.x2 W W e.x3 t.y2 e.x4 t.y3 W e.x5;
}


Loop_12_3 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (W e.x4) =  <Loop_12_3 (e.x1) t.y1 (e.x2) t.y2 (e.x3 W) (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (t.y3 W e.x4) =  <Loop_12_4 (e.x1) t.y1 (e.x2 t.y2 e.x3 W W) t.y3 (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (e.x4 t.y3 t.y4 W e.x5) =  <Loop_12_4 (e.x1) t.y1
                                                              (e.x2 t.y2 e.x3 W W e.x4 t.y3) t.y4 (e.x5)
                                                           >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (e.x4) =  e.x1 t.y1 W S W e.x2 t.y2 e.x3 W W e.x4;
}


Loop_12_4 {
 (e.x1) t.y1 (e.x2) t.y2 (W e.x3) =  <Loop_12_3 (e.x1) t.y1 (e.x2) t.y2 () (e.x3)>;
 (e.x1) t.y1 (e.x2) t.y2 (t.y3 W e.x3) =  <Loop_12_4 (e.x1) t.y1 (e.x2 t.y2 W) t.y3 (e.x3)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3 t.y3 t.y4 W e.x4) =  <Loop_12_4 (e.x1) t.y1
                                                       (e.x2 t.y2 W e.x3 t.y3) t.y4 (e.x4)
                                                    >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) =  e.x1 t.y1 W S W e.x2 t.y2 W e.x3;
}


Loop_12_5 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (W e.x5) =  <Loop_12_5 (e.x1) t.y1 (e.x2) t.y2
                                                           (e.x3) t.y3 (e.x4 W) (e.x5)
                                                        >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (t.y4 W e.x5) =  <Loop_12_6 (e.x1) t.y1 (e.x2)
                                                                t.y2 (e.x3 t.y3 e.x4 W W) t.y4 (e.x5)
                                                             >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (e.x5 t.y4 t.y5 W e.x6) =  <Loop_12_6 (e.x1) t.y1 (e.x2)
                                                                          t.y2 (e.x3 t.y3 e.x4 W
                                                                                  W e.x5 t.y4
                                                                               ) t.y5 (e.x6)
                                                                       >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (e.x5) =  e.x1 t.y1 W S W e.x2 t.y2 e.x3 t.y3 e.x4 W W e.x5;
}


Loop_12_6 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (W e.x4) =  <Loop_12_5 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 () (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (t.y4 W e.x4) =  <Loop_12_6 (e.x1) t.y1 (e.x2)
                                                         t.y2 (e.x3 t.y3 W) t.y4 (e.x4)
                                                      >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4 t.y4 t.y5 W e.x5) =  <Loop_12_6 (e.x1) t.y1 (e.x2)
                                                                   t.y2 (e.x3 t.y3 W e.x4 t.y4) t.y5 (e.x5)
                                                                >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) =  e.x1 t.y1 W S W e.x2 t.y2 e.x3 t.y3 W e.x4;
}


Loop_12_7 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (W e.x4) =  <Loop_12_7 (e.x1) t.y1 (e.x2) t.y2 (e.x3 W) (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (t.y3 W e.x4) =  <Loop_12_8 (e.x1) t.y1 (e.x2 t.y2 e.x3 W W) t.y3 (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (e.x4 t.y3 t.y4 W e.x5) =  <Loop_12_8 (e.x1) t.y1
                                                              (e.x2 t.y2 e.x3 W W e.x4 t.y3) t.y4 (e.x5)
                                                           >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) (e.x4) =  e.x1 t.y1 W S e.x2 t.y2 e.x3 W W e.x4;
}


Loop_12_8 {
 (e.x1) t.y1 (e.x2) t.y2 (W e.x3) =  <Loop_12_7 (e.x1) t.y1 (e.x2) t.y2 () (e.x3)>;
 (e.x1) t.y1 (e.x2) t.y2 (t.y3 W e.x3) =  <Loop_12_8 (e.x1) t.y1 (e.x2 t.y2 W) t.y3 (e.x3)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3 t.y3 t.y4 W e.x4) =  <Loop_12_8 (e.x1) t.y1
                                                       (e.x2 t.y2 W e.x3 t.y3) t.y4 (e.x4)
                                                    >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) =  e.x1 t.y1 W S e.x2 t.y2 W e.x3;
}


Loop_12_9 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (W e.x5) =  <Loop_12_9 (e.x1) t.y1 (e.x2) t.y2
                                                           (e.x3) t.y3 (e.x4 W) (e.x5)
                                                        >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (t.y4 W e.x5) =  <Loop_12_10 (e.x1) t.y1 (e.x2)
                                                                t.y2 (e.x3 t.y3 e.x4 W W) t.y4 (e.x5)
                                                             >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (e.x5 t.y4 t.y5 W e.x6) =  <Loop_12_10 (e.x1) t.y1 (e.x2)
                                                                          t.y2 (e.x3 t.y3 e.x4 W
                                                                                  W e.x5 t.y4
                                                                               ) t.y5 (e.x6)
                                                                       >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) (e.x5) =  e.x1 t.y1 W S e.x2 t.y2 e.x3 t.y3 e.x4 W W e.x5;
}


Loop_12_10 {
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (W e.x4) =  <Loop_12_9 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 () (e.x4)>;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (t.y4 W e.x4) =  <Loop_12_10 (e.x1) t.y1 (e.x2)
                                                         t.y2 (e.x3 t.y3 W) t.y4 (e.x4)
                                                      >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4 t.y4 t.y5 W e.x5) =  <Loop_12_10 (e.x1) t.y1 (e.x2)
                                                                   t.y2 (e.x3 t.y3 W e.x4 t.y4) t.y5 (e.x5)
                                                                >;
 (e.x1) t.y1 (e.x2) t.y2 (e.x3) t.y3 (e.x4) =  e.x1 t.y1 W S e.x2 t.y2 e.x3 t.y3 W e.x4;
}

/* This file is generated by MSCP at Tue Aug 24 19:54:02 2021.*/

/* Elapsed time of embeddings is 31.0.*/

/* Elapsed time of generalizations is 7123.0.*/

Скачать: rsd_bloat-basic.ref.

Видно, что получилось 11 базисных конфигураций. Так что можно ожидать, что при использовании перестройки сверху получится около десятка экземпляров, а не 56, как сейчас. Уже неплохо.

Перестройка снизу часто строит экземпляры, соответствующие развёрнутым виткам цикла. Эти витки затем подставляются на этапе прогонки экземпляров и тем самым раздувают программу. Перестройка сверху избегает развёртки витков (по сравнению с перестройкой снизу), на этапе прогонки экземпляров встраиваний должно быть меньше.

Mazdaywik avatar Aug 24 '21 18:08 Mazdaywik

imho перестройка сверху точно нужна: здесь явный комбинаторный взрыв. Какая именно из двух --- вот не знаю.

TonitaN avatar Aug 24 '21 18:08 TonitaN

Почему у меня рефальские исходники, упомянутые в этой заявке, качаются с дополнительным расширением txt? Баг или фича?

TonitaN avatar Aug 24 '21 18:08 TonitaN

imho перестройка сверху точно нужна: здесь явный комбинаторный взрыв. Какая именно из двух — вот не знаю.

Очевидно, халтурная. Я хочу поскорее выпустить версию 3.4.

Почему у меня рефальские исходники, упомянутые в этой заявке, качаются с дополнительным расширением txt? Баг или фича?

Это фича. Прикрепить к комментариям можно только файлы с несколькими разрешёнными расширениями: image

Крупнее: image

Поэтому мне приходится к именам исходников добавлять .txt. Если попробовать приложить файл с другим расширением, сайт ругается: image

Mazdaywik avatar Aug 24 '21 18:08 Mazdaywik

Вывод

Буду делать халтурную перестройку сверху. @TonitaN, спасибо!

Mazdaywik avatar Aug 24 '21 19:08 Mazdaywik

Да не за что, ты же и сам пришел к тому же выводу. Я повтыкала в конфигурации Loop-а, и всё 🤓.

TonitaN avatar Aug 24 '21 19:08 TonitaN

Ну, асилила многабукаф. Ну, и ты могла прийти и к другому выводу.

Кстати, поведение MSCP-A на этом примере ожидаемо?

Вот этот комментарий https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-901267648 пыталась читать?

Mazdaywik avatar Aug 24 '21 19:08 Mazdaywik

Да, поведение ожидаемо. Комментарий не читала, кстати, неочевидные утверждения из него пока что мне не очевидны. Для дерева (бесконечного) они, понятное дело, верны. А вот что касается графа --- сходу нет интуиции, что при перестройке снизу одна из конфигураций после обобщения не может обобщиться с какой-то из тех, которые находятся на отрезке от верхней (не обобщённой) до нижней конфигурации. Тогда уже может пойти развитие совсем другой истории.

Да, это оффтопик, надо было написать ответ к тому комментарию.

TonitaN avatar Aug 24 '21 19:08 TonitaN

А я ждал комментарий там 😊.

Mazdaywik avatar Aug 24 '21 19:08 Mazdaywik

Ты лучше туда скопируй комментарий, я на него отвечу.

Mazdaywik avatar Aug 24 '21 19:08 Mazdaywik

Предыдущие коммиты проблему не исправили

Шаг в правильном направлении был сделан, но этого оказалось мало.

«Халтурная» перестройка сверху, с одной стороны, уменьшила размер лога bloat-basic.log, теперь он весит 6,3 Мбайт (ранее 11 Мбайт), и уменьшила размер остаточной программы (residual.txt) до 6 483 строк (ранее 15 555).

С другой этого оказалось недостаточно для того, чтобы автотесты стали проходить (см. коммит перед этим комментарием).

В процессе «халтурных» обобщений ранее специализированные экземпляры подменяются на вызов более позднего экземпляра:

  /* Cold by SPEC-PATCHED */
  Loop@3 {
    (e.0) t.1 t.2 e.3 = <Loop@8 (e.0) t.1 W S t.2 e.3>;
  }

Затем, на проходе специализации экземпляров эти функции тривиально встраиваются. (Заметим, что теперь специализация может увеличивать число шагов рефал-машины).

Собственно, поэтому она и халтурная.

Таких «перестроенных» экземпляров в остаточной программе (до прогонки экземпляров) оказалось 24 (из 61 экземпляра всего).

Что делать дальше?

Пока не знаю.

Отношение остановки SCP4

Возможный вариант — ослабить отношение остановки, приблизив его к «упрощающему отношению» SCP4: image Красным цветом я зачеркнул очевидные опечатки.

Отношение остановки SCP4 позволяет взаимозаменять s- и t-параметры с символами, а также игнорирует все e-параметры в исторической конфигурации (следует из правила «если pd+ ≥ pd′+ pd″+, то pd+ ≥ pd′+ e.name pd″+). Для ряда историй оно было бы актуальным. Например:

Fri Sep 03 15:10:31 2021: History of Loop@33
    START@0: [(e.0) t.1 (e.2)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@2: [(e.0 t.1 W) S W e.2]
    Loop@6: [(e.0 t.1 W S W) t.2 W e.3]
    Loop@20: [(e.0 t.1 s.2 s.3 t.4 t.5) W W e.6]
    Loop@33: [(e.0 t.1 s.2 s.3 t.4 t.5 W W) t.6 W e.7]

Здесь бы Loop@33 обобщилась бы с Loop@2.

В актуальной реализации для ускорения проверки условия остановки отношение Хигмана-Крускала предваряется отношением Хигмана, т.е. отношением подпоследовательностей на цепочках токенов. Отношение Хигмана проверяется быстро, за линейное время O(|s| + |t|), поэтому если оно не выполняется, то заведомо более дорогое отношение Хигмана-Крускала (O(|s|×|t|/log(|t|) + |t|×log(|t|)), см. статью) можно не вычислять (т.к. второе влечёт первое). (Оптимизация не умозрительная, ускорение проверки отношения было очевидно по профилю.)

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

Более грамотная чистка от неиспользуемых функций (см. #228)

Функции вида

  /* Cold by SPEC-PATCHED */
  Loop@3 {
    (e.0) t.1 t.2 e.3 = <Loop@8 (e.0) t.1 W S t.2 e.3>;
  }

остаются в синтаксическом дереве и затем на этапе прогонки экземпляров оптимизируются. Хотя они могут оказаться неиспользуемыми и после чистки в финальное дерево не попадут (конкретно Loop@3 попадает, т.к. функция START прогоняется не до конца — есть ограничение на размер и глубину дерева прогонки).

Так что оптимизация (в частности прогонка) на последнем этапе должна быть ленивой — не должна оптимизировать те функции, которые ни разу не вызываются.

Либо выделить вспомогательный проход прогонки только перестроенных функций. Эти функции заведомо прогоняются (по построению форматы аргументов экземпляров всегда правильные), и будут прогоняться даже при поддержке активных аргументов (#230), такой проход может заранее очистить дерево от ненужного мусора. И этот проход можно даже включать для режима -OS без -OD.

Настало время удивительных историй

котолампа

Попробовал я оптимизировать остаточную программу rsd_bloat-basic.ref, построенную суперкомпилятором MSCP-A. Гипотеза: если мы уже имеем оптимизированную программу, в которой выделены базисные конфигурации, то повторная суперкомпиляция должна дать тривиальный результат. Но оказалось всё интереснее.

Компилятор начал создавать экземпляры для функций-базисных конфигураций, это в целом ожидаемо. Интересное поджидало в логе.

Если я правильно понимаю суперкомпиляцию, то в полностью факторизованном графе в историях конфигураций не должно быть пар, связанных отношением остановки. Т.е. если история конфигурации Cn (т.е. путь от корня до неё) имеет вид C0, C1, …, Cn, то в нём не должно быть таких i < j, что Ci ≤ Cj, потому что иначе бы случилась перестройка.

@TonitaN, я правильно понимаю суперкомпиляцию?

А вот что у меня получилось в логе:

Fri Sep 03 14:22:19 2021: History of Loop_12_9@8
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@3: [(e.0) t.1 (e.2) t.3 (e.4 t.5) t.6 (e.7)]
    Loop_12_9@8: [(e.0) t.1 (e.2) t.3 (e.4 t.5) t.6 (e.7) (e.8)]

Fri Sep 03 14:22:19 2021: History of Loop_12_3@9
    Loop_12_3@0: [(e.0) t.1 (e.2) t.3 (e.4) (e.5)]
    Loop_12_4@4: [(e.0) t.1 (e.2 t.3 W) t.4 (e.5)]
    Loop_12_3@9: [(e.0) t.1 (e.2 t.3 W) t.4 (e.5) (e.6)]

Fri Sep 03 14:22:19 2021: History of Loop_12_5@9
    Loop_12_5@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_6@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_5@9: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7) (e.8)]

Fri Sep 03 14:22:19 2021: History of Loop_12_7@9
    Loop_12_7@0: [(e.0) t.1 (e.2) t.3 (e.4) (e.5)]
    Loop_12_8@4: [(e.0) t.1 (e.2 t.3 W) t.4 (e.5)]
    Loop_12_7@9: [(e.0) t.1 (e.2 t.3 W) t.4 (e.5) (e.6)]

Fri Sep 03 14:22:19 2021: History of Loop_12_9@9
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@9: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7) (e.8)]

Куча экземпляров имеют неправильные истории. Например, если в последней сигнатуре для Loop_12_9@9 стереть некоторые элементы, получим сигнатуру Loop_12_9@0. Для других аналогично.

Тут нужно пояснить, что такое Func@0 на дне истории, да и вообще, что такое история экземпляра.

Специализация может зациклиться. Пусть в функции F вызывается рекурсивная функция G. Для её вызова будет создан экземпляр G@1. Функция рекурсивная, поэтому для рекурсивного вызова может быть создан новый экземпляр G@2. При специализации рекурсивного вызова в G@2 будет создан новый экземпляр G@3. В результате получим бесконечную цепочку экземпляров, которая прерывается по отношению остановки (здесь: Хигмана-Крускала).

Чтобы иметь возможность прерывать цепочки специализаций, для каждого экземпляра формируется история. Если экземпляр F@n впервые возник из вызова функции F в экземпляре G@m, то история экземпляра F@n состоит из истории экземпляра G@m + сигнатуры F@n. Если экземпляр F@n возник из вызова внутри не-экземпляра, то его история состоит из одной только своей сигнатуры, иначе говоря, истории не-экземпляров пустые.

Особый случай — когда специализируются вызовы внутри самой специализируемой функции. Оказалось, что в этом случае в самой функции (если у неё в формате есть переменные-аккумуляторы) начинают формироваться совершенно бестолковые экземпляры, соответствующие развёртыванию одного витка цикла. Пришлось для таких случаев искусственно формировать историю, на дне которой лежит тривиальная сигнатура — сигнатура, построенная как обобщение образцов всех предложений. Такой сигнатуре приписывалось имя несуществующего экземпляра Func@0 (реальные экземпляры нумеруются начиная с 1). В этом случае избыточные экземпляры уже не генерируются.

В старом коде (до реализации «халтурной» перестройки сверху) при зацикливании между текущим вызовом и сигнатурой для Func@0 вычислялось обобщение, оно неизбежно оказывалось тривиальной сигнатурой (обобщением образцов всех предложений), а для тривиальной сигнатуры вызов не специализируется.

В новом коде получилась вот такая фигня:

Fri Sep 03 14:22:19 2021: History of Loop_12_9@9
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@9: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7) (e.8)]

Как же она получилась?

Экземпляр Loop_12_9@9 возник внутри экземпляра Loop_12_9@7:

  Loop_12_9@7 {
    (e.X) t.X (e.X1) t.X1 (e.X2) t.X2 t.X3 W e.X5
      = <Loop_12_9 (e.X) t.X (e.X1) t.X1 (e.X2 t.X2 W) t.X3 (W) (e.X5)>;    /* ❗ */

    (e.X) t.X (e.X1) t.X1 (e.X2) t.X2 t.X3 t.X4 W e.X6
      = <Loop_12_10 (e.X) t.X (e.X1) t.X1 (e.X2 t.X2 W t.X3 W W) t.X4 (e.X6)>;

    (e.X) t.X (e.X1) t.X1 (e.X2) t.X2 t.X3 e.X5 t.X6 t.X7 W e.X9
      = <Loop_12_10
          (e.X) t.X (e.X1) t.X1 (e.X2 t.X2 W t.X3 W W e.X5 t.X6) t.X7 (e.X9)
        >;

    (e.X) t.X (e.X1) t.X1 (e.X2) t.X2 t.X3 e.X4
      = e.X t.X W S e.X1 t.X1 e.X2 t.X2 W t.X3 W W e.X4;
  }

История этого экземпляра:

Fri Sep 03 14:22:19 2021: History of Loop_12_9@7
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@7: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 () (e.7)]

При специализации первого вызова формируется история:

    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@7: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 () (e.7)]
    _____________: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7) (e.8)]

Для двух последних строчек срабатывает отношение Хигмана-Крускала (действительно, e.7 можно стереть) — вычисляется обобщение. История для обобщённого экземпляра строится из усечённой истории экземпляра Loop_12_9@7, т.е. без Loop_12_9@7 + новая обобщённая сигнатура. Выполняется перестройка сверху — экземпляр заменяется на

  /* Cold by SPEC-PATCHED */
  Loop_12_9@7 {
    (e.0) t.1 (e.2) t.3 (e.4) t.5 t.6 e.7
      = <Loop_12_9@9 (e.0) t.1 (e.2) t.3 (e.4) t.5 t.6 () e.7>;
  }

Но для новой истории

Fri Sep 03 14:22:19 2021: History of Loop_12_9@9
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@9: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7) (e.8)]

никаких проверок не выполняется, и получается такая фигня.

Правильнее для Loop_12_9@9 вообще экземпляр не строить, а Loop_12_9@7 зацикливать на тривиальную сигнатуру. Но мне пока не очевидно, как это красиво сделать в коде небольшими правками.

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

C0, C1, …, Ci, …, Cj, …, Ck

причём ! (Ci ≤ Cj) и Cj ≤ Ck, то после обобщения Cg = GEN(Cj, Ck) и перестройки истории

C0, C1, …, Ci, …, Cg

может оказаться Ci ≤ Cg.

Например, была история

С1 = <F e.X ()>, С2 = <F A (Z)>, С3 = <F A B (Z)>

Для C1 и C2 условие остановки не срабатывает — нельзя ничего стереть в <F A> и получить <F e.X>. Для C2 и C3 срабатывает (можно стереть B). Строим обобщение:

C1 = <F e.X ()>, C4 = <F A e.X (Z)>

и тут условие остановки для C1 и C4 сработает: в C4 можно стереть A и Z и получить C1!

@TonitaN, ты знала об этом?

Возможно, расширение отношения Хигмана-Крускала в SCP4 обусловлено желанием сделать условие остановки более монотонным, т.е. избегать такого каскада перестроек. Действительно, по упрощающему отношению SCP4 можно в нижней конфигурации не только стирать элементы, но и заменять произвольные участки на e-параметры. В C2 можно стереть Z и заменить A на e-параметр и получить C1.

И по упрощающему отношению SCP4 в истории

Fri Sep 03 14:22:19 2021: History of Loop_12_9@7
    Loop_12_9@0: [(e.0) t.1 (e.2) t.3 (e.4) t.5 (e.6) (e.7)]
    Loop_12_10@4: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 (e.7)]
    Loop_12_9@7: [(e.0) t.1 (e.2) t.3 (e.4 t.5 W) t.6 () (e.7)]

сигнатура экземпляра @7 сводилась бы к @0, т.к. пустоту в предпоследних скобках можно заменить на e-параметр.

К слову, для исходного теста bloat-basic.ref рассуждения выше не актуальны — при любых обобщениях сохраняется инвариант.

Что делать?

Если делать нормальную перестройку сверху, как описано в https://github.com/bmstu-iu9/refal-5-lambda/issues/332#issuecomment-901267648, то там подобный каскад обобщений будет получаться совершенно естественно.

В актуальной реализации можно в проверку отношения остановки добавить вычисление обобщения + цикл.

Mazdaywik avatar Sep 03 '21 16:09 Mazdaywik

@Mazdaywik , кстати, нигде не видела такого требования к графу суперкомпиляции, чтобы на его путях не было выполнено Ci<=Cj. Наверное, с точки зрения теории, эту формулировку просто проглядели, потому что условие вложимости конфигураций всех интересовало прежде всего с точки зрения завершаемости, а оно (свойство wqo "нет бесконечных антицепей") работает на любом отрезке бесконечной развертки, т.е. можно спокойно отбрасывать любой начальный отрезок бесконечного пути.

TonitaN avatar Sep 03 '21 21:09 TonitaN

Определение. Let-экземпляр — экземпляр вида

Func@k {
  ARG = <Func@m ARG′>
}

При халтурной перестройке сверху старый экземпляр становится Let-экземпляром.

Предлагается следующий вариант алгоритма специализации:

  • Строится для вызова сигнатура.
  • Если сигнатура тривиальная — вызов не оптимизируется.
  • Если сигнатура известная, то вызывается ранее построенный экземпляр.
  • Если сигнатура новая — строится новый экземпляр. Т.е. инкрементируется счётчик экземпляров и формируется вызов Func@k. Для новой сигнатуры экземпляр строится всегда. Далее.
    • ПРЫГ СЮДА:
    • Если сигнатура тривиальная — строится let-экземпляр, вызывающий тривиальную сигнатуру (на первом витке такое невозможно).
    • Если условие остановки не сработало — строится обычный экземпляр.
    • Если сработало условие остановки и текущая сигнатура Func@k является уточнением старой — генерируется let-экземпляр, вызывающий старую сигнатуру.
    • Если сработало условие остановки и текущая сигнатура Func@k не является уточнением старой Func@m, строится обобщающая сигнатура Func@n = GEN(Func@k, Func@m), строится let-экземпляр Func@k, экземпляр Func@m заменяется на let-экземпляр, текущей сигнатурой становится Funk@n, GOTO «ПРЫГ СЮДА».

Во-первых, данный алгоритм решит вторую проблему из моего предыдущего комментария — будет работать каскад обобщений.

Во-вторых, код должен немного упроститься — мы сразу построим вызов функции для данной сигнатуры и дальше уже таскать подстановку не нужно будет.

Недостаток алгоритма — лишние let-экземпляры. Эти экземпляры можно устранять отдельным проходом прогонки, выполняемым после цикла специализации. Он будет выполняться всегда, даже если ключ -OD не указан. В результате, во-первых, лишних экземпляров не будет (отчасти решит и первую проблему моего предыдущего комментария), во-вторых, специализация не будет увеличивать число шагов рефал-машины.


А для решения первой проблемы нужно ослаблять условие остановки.

Mazdaywik avatar Sep 10 '21 14:09 Mazdaywik

Промежуточные выводы

Реализована «халтурная» перестройка сверху. Let-экземпляры теперь встраиваются, после встраивания let-экземпляров программа чистится от избыточных функций.

Некоторые выводы.

Тест test-10_Mon-Aug-23-21-51-16-UTC-2021.ref проходит

Случайный автотест test-10_Mon-Aug-23-21-51-16-UTC-2021.ref стал проходить. Уже хорошо. Одна из целей данной заявки (чтобы прошёл этот тест) достигнута. Однако, это ещё не всё.

Прогонка с активными аргументами (#230)

В процессе тестирования перестройки сверху один из автотестов (varcopy-fail.ref) стал вылетать по лимиту шагов. Не компилятор, а сам тест. В логе были обнаружены невстроенные вызовы let-экземпляров — они не встроились из-за того, что аргументы вызовов были активными. Я решил, что выход за лимит числа шагов произошёл только из-за этих избыточных шагов для let-экземпляров.

Тогда я реализовал #230 (она оказалась даже проще, чем я думал). Вызовы экземпляров стали встраиваться. Не помогло. Проблема оказалась в том, что получался рекурсивный let-экземпляр. Исправлено в коммите 9694ceb67e44457c0da6b323ed713d9985e60188.

Анализ bloat-basic.ref

Объём лога компиляции теперь составляет 3956 Кбайт. Сам лог: bloat-basic.log.

Можно выделить три «остаточные» программы:

  • Программа после проходов прогонки и специализации, но до встройки let-экземпляров и чистки неиспользуемых функций: bloat-basic-1-after-spec.txt, её размер — 810 строк, в ней 143 экземпляра функции Loop.
  • Программа после встраивания let-экземпляров и чистки неиспользуемых функций: bloat-basic-2-after-cleanup.txt, её размер — 173 строки, остались 12 экземпляров функции Loop. Интересно здесь то, что число экземпляров примерно совпадает с числом конфигураций в остаточной программе MSCP-A (rsd_bloat-basic.ref) — 11 штук Loop_12_n + 1 вспомогательная функция InputFormat_0. Скорее всего, это совпадение.
  • Программа после прогонки экземпляров: bloat-basic-3-after-tree-opt.txt, её размер 4773 строки, в ней осталось 10 экземпляров (встроились Loop@1 и @3) + добавились 12 остатков экземпляров Loop@n*2. Этот вопрос мы подробнее опишем в следующем разделе.

Интересным представляется следующее наблюдение.

В первоначальном варианте (bloat-basic.log, который 11 Мбайт) есть функция Loop@4:

Tue Aug 24 18:00:43 2021: History of Loop@4
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@4: [(e.0 t.1) t.2 W e.3]

которая затем является родоначальницей экземпляра Loop@9:

Tue Aug 24 18:00:47 2021: History of Loop@9
    START@0: [(e.1) t.2 (e.3)]
    Loop@1: [(e.0) t.1 W S e.2]
    Loop@4: [(e.0 t.1) t.2 W e.3]
    Loop@9: [(e.0 t.1 t.2) W W e.3]

В новом варианте функция с этой же сигнатурой получается из Loop:

  Loop {
    (e.Acc) e.Begin t.U t.V W e.End = <Loop@2 (e.Acc e.Begin) t.U t.V e.End>;

    (e.Acc) e.Rest = e.Acc e.Rest;
  }

  . . .

  /* Cold by LET */
  Loop@2 {
    (e.Acc1) t.U t.V e.End = <Loop (e.Acc1 t.U) t.V W e.End>;
  }
Tue Sep 28 09:50:10 2021: History of Loop@2
    Loop@2: [(e.0 t.1) t.2 W e.3]

И затем, когда та же сигнатура косвенно возникает при специализации из функции START, она уже не порождает новый экземпляр, а вызывает этот let-экземпляр. Такая вот косая стрелка.

Про прогонку экземпляров

Файлы bloat-basic.ref и bloat-condition.ref автотестами сделать не удалось — компилятору не хватает лимита шагов.

Во-первых, для основных автотестов он меньше, чем для случайных, причём меньше в 10 раз (20 000 000 против 200 000 000). Во-вторых, во время автотестов формируется лог компиляции, требующий на свой вывод дополнительные шаги (для случайных тестов не формируется).

Анализ дампа показывает, что лимит шагов истекает на стадии прогонки экземпляров.

А прогонка экземпляров в этом примере здорово взрывает остаточную программу.

  • Исходно 835 строк взрывались до 15 555.
  • Сейчас 173 строки взрываются до 4773.

И возникает вопрос — а зачем нам нужна прогонка экземпляров?

Исходно она нужна была для борьбы с несовершенством оптимизаций: специализация не умела прогонять, а прогонка не умела работать с рекурсивными функциями. Оптимизируемые интерпретаторы приходилось разбивать на две функции — одна специализируется по интерпретируемой программе, вторая посредством прогонки анализирует данные, например

https://github.com/bmstu-iu9/refal-5-lambda/blob/331442a7def29f9d89190ee5dedca7dc9d3a93ac/src/compiler/OptTree.ref#L226-L271

Другой пример — в записке @Kaelena: РПЗ_Калинина_Автоматическая разметка оптимизируемых_функций_2020.pdf.

В результате получалось множество экземпляров, большинство из которых были транзитными — их прогонка не требовала сужений. А в случае простых интерпретаторов, нетранзитные тоже имело смысл прогонять.

Сейчас такой потребности нет — интерпретатор можно схлопнуть в одну функцию, пометить её *$OPT и её вызовы будут либо прогоняться, либо специализироваться. Ну, в теории, я пока не пробовал на самом деле. А значит, лишних экземпляров быть не должно или их должно быть гораздо меньше.

Так что, возможно, стоит отказаться от этого прохода, или хотя бы внимательно проанализировать её плюсы и минусы.

Mazdaywik avatar Sep 29 '21 06:09 Mazdaywik

Настало время удивительных историй

котолампа.png

Самоприменение с ключами

set RLMAKE_FLAGS=-X-OiADPRS -X--log=__srefc-core.log
Sun Oct 03 21:05:05 2021: History of DoTokenChain-AddRedefinition*1@38
    DoTokenChain-AfterCall$4=2@0: ["s.Mode:" s.0 "e.Collected:" (e.1) "e.OptionalFuncName:" (e.2) "e.BracketTerms:" (e.3) "s.Type:" s.4 "t.Pos:" t.5 "e.Value:" (e.6) "e.Tokens:" (e.7) t.8]
    DoTokenChain@21: [s.0 Pattern t.1 (e.2 (Brackets e.3) (Symbol Identifier e.4)) e.5]
    DoTokenChain:1@21: ["s.Mode:" s.0 "s.Kind:" Pattern "t.ErrorList:" t.1 "e.Collected:" (e.2 (Brackets e.3) (Symbol Identifier e.4)) "e.Tokens:" (e.5) t.6]
    DoTokenChain-AfterCall*1@114: [s.0 Pattern (e.1 (s.2 e.3) (s.4 t.5 e.6)) t.7 ((Symbol Name t.8 e.9)) e.10]
    DoTokenChain-AfterCall$4=1@126: ["s.Mode:" s.0 "e.Collected:" (e.1 (s.2 e.3) (s.4 t.5 e.6)) "e.OptionalFuncName:" ((Symbol Name t.7 e.8)) "e.BracketTerms:" (e.9) "s.Type:" s.10 "t.Pos:" t.11 "e.Value:" (e.12) "e.Tokens:" (e.13) e.14]
    DoTokenChain-AfterCall$4=2@112: ["s.Mode:" s.0 "e.Collected:" (e.1 (s.2 e.3) (s.4 t.5 e.6)) "e.OptionalFuncName:" ((Symbol Name t.7 e.8)) "e.BracketTerms:" (e.9) "s.Type:" s.10 "t.Pos:" t.11 "e.Value:" (e.12) "e.Tokens:" (e.13) e.14]
    DoTokenChain:1*11@105: ["s.Mode:" s.0 "s.Kind:" Pattern "t.ErrorList:" t.1 "e.Collected:" (e.2 (s.3 e.4) (s.5 t.6 e.7) (Brackets (Symbol Name t.8 e.9) e.10)) "e.Tokens:" (e.11) (s.12 t.13 e.14)]
    DoTokenChain-AddRedefinition*1@38: [Pattern e.0 (e.1 (s.2 e.3) (s.4 t.5 e.6) (Brackets (Symbol Name t.7 e.8) e.9)) t.10]

Очевидно, что сигнатура DoTokenChain-AfterCall$4=2@112 должна вложиться в DoTokenChain-AfterCall$4=2@0, но она не вложилась, а история продолжилась.

Mazdaywik avatar Oct 03 '21 18:10 Mazdaywik

История не удивительная

История не удивительная:

Sun Oct 03 21:05:05 2021: History of DoTokenChain-AddRedefinition*1@38
    DoTokenChain-AfterCall$4=2@0: [… "e.Tokens:" (e.7) t.8]
    …
    DoTokenChain-AfterCall$4=2@112: [… "e.Tokens:" (e.13) e.14]
    …

Если приглядеться внимательнее, то сигнатура DoTokenChain-AfterCall$4=2@112 заканчивается на (e.13) e.14, что, очевидно, не упрощается до (e.7) t.8, переменные разные.

Mazdaywik avatar Oct 06 '21 18:10 Mazdaywik