Falujący

W informatyce , w szczególności w zautomatyzowanym dowodzeniu twierdzeń , falowanie odnosi się do grupy heurystyk metapoziomowych , opracowanych głównie w Grupie Rozumowania Matematycznego w Szkole Informatyki na Uniwersytecie w Edynburgu i najczęściej używanej do prowadzenia dowodów indukcyjnych w zautomatyzowanych systemy dowodzenia twierdzeń . Falowanie można postrzegać jako ograniczoną formę systemu przepisywania , gdzie stosowane są specjalne adnotacje na poziomie obiektu, aby zapewnić zapłodnienie po zakończeniu przepisywania, z wymogiem zmniejszającym miarę zapewniającym zakończenie dowolnego zestawu reguł i wyrażeń przepisywania.

Historia

Raymond Aubin był pierwszą osobą, która użyła terminu „falowanie” podczas pracy nad swoją rozprawą doktorską z 1976 roku na Uniwersytecie w Edynburgu. Rozpoznał powszechny wzorzec ruchu na etapie przepisywania dowodów indukcyjnych. Alan Bundy wywrócił później tę koncepcję do góry nogami, definiując falowanie jako wzorzec ruchu, a nie efekt uboczny.

Od tego czasu ukuto określenia „falowanie na boki”, „falowanie w” i „falowanie przeszłości”, więc termin ten uogólniono na falowanie. Od 2007 roku Rippling jest nadal rozwijany w Edynburgu i gdzie indziej.

Falowanie zastosowano do wielu problemów tradycyjnie postrzeganych jako trudne w środowisku dowodzącym twierdzeń indukcyjnych, w tym do twierdzeń granicznych Bledsoe’a [ i dowodu działania mikroprocesora Gordona, miniaturowego komputera opracowanego przez Michaela JC Gordona i jego zespół w Cambridge.

Przegląd

Bardzo często, próbując udowodnić twierdzenie, otrzymujemy wyrażenie źródłowe i wyrażenie docelowe, które różnią się jedynie dodatkiem kilku dodatkowych elementów składniowych.

Jest to szczególnie prawdziwe w dowodach indukcyjnych , gdzie dane wyrażenie przyjmuje się za hipotezę indukcyjną , a wyrażenie docelowe za wniosek indukcyjny. Zwykle różnice między hipotezą a wnioskiem są jedynie niewielkie i mogą obejmować włączenie funkcji następczej (np. +1) wokół zmiennej indukcyjnej.

Na początku falowania identyfikowane są różnice między tymi dwoma wyrażeniami, zwane w języku falującym frontami fal. Zazwyczaj różnice te uniemożliwiają ukończenie dowodu i należy je „odsunąć”. Do docelowego wyrażenia dodano adnotację, aby rozróżnić fronty falowe (różnice) i szkielet (wspólną strukturę) pomiędzy dwoma wyrażeniami. Specjalne reguły, zwane regułami falowymi, mogą być następnie użyte w kończący do manipulowania wyrażeniem docelowym, dopóki wyrażenie źródłowe nie będzie mogło zostać użyte do zakończenia dowodu.

Przykład

Naszym celem jest pokazanie, że dodawanie liczb naturalnych jest przemienne . Jest to własność elementarna i dowód przeprowadza się za pomocą indukcji rutynowej. Niemniej jednak przestrzeń poszukiwań takiego dowodu może być dość duża.

Zazwyczaj podstawowy przypadek dowolnego dowodu indukcyjnego rozwiązuje się metodami innymi niż falowanie. Z tego powodu skupimy się na przypadku krokowym. Nasz przypadek krokowy ma następującą postać, w której zdecydowaliśmy się użyć x jako zmiennej indukcyjnej:

Możemy także posiadać kilka reguł przepisywania, zaczerpniętych z lematów, definicji indukcyjnych lub innych źródeł, które można wykorzystać do utworzenia reguł falowych. Załóżmy, że mamy następujące trzy reguły przepisywania:

następnie można je opatrzyć adnotacjami, tworząc:

Zauważ, że wszystkie te reguły z adnotacjami zachowują szkielet (x + y = y + x w pierwszym przypadku i x + y w drugim/trzecim). Teraz, opisując przypadek kroku indukcyjnego, otrzymujemy:

I jesteśmy gotowi do wykonania falowania:

Należy zauważyć, że ostateczne przepisanie powoduje zniknięcie wszystkich frontów fal i możemy teraz zastosować zapłodnienie, czyli zastosowanie hipotez indukcyjnych, aby zakończyć dowód.

Dalsza lektura

•   David A. Basin i Toby Walsh (1996). „Rachunek i zakończenie falowania” (PDF) . Journal of automatycznego rozumowania . 16 (1–2): 147–180. doi : 10.1007/BF00244462 . S2CID 14427821 .