Spędziłem tydzień lub dwa programując proste rozwiązanie logiczne. Po zbudowaniu tego zastanawiałem się, czy język, który rozwiązuje, to Turing-complete, czy nie. Tak więc zakodowałem mały zestaw równań, które akceptują dowolną prawidłową ekspresję w rachunku kombinatorycznym SKI i tworzą zestaw wyników, który zawiera normalną formę tego wyrażenia. Ponieważ SKI to Turing-complete, udowodnienie, że mój język może wykonać SKI, zademonstruje jego kompletność Turinga.Czy mój program Turing-complete?
Istnieje jednak usterka. Solver nie redukuje wyrażenia w normalnej kolejności. W rzeczywistości to, co można zrobić, to wypróbować każde możliwe zamówienie redukcji. Co oznacza, że zestaw rozwiązań jest zwykle ogromny. Jeśli istnieje normalna forma, będzie tam gdzieś, ale trudno powiedzieć gdzie.
To prowadzi mnie do dwóch pytań:
Czy mój język Turing-zupełny? Czy muszę znaleźć lepszy dowód?
Czy liczba rozwiązań jest funkcją obliczalną danych wejściowych?
(Początkowo założono, że wielkość zestawu Roztwór wykładniczy lub silnia w wielkości wejściowej. Ale przy bliższym, to nie jest prawda. Można pisać ogromne wyrażeń, które są już w postaci normalnej, i małe wyrażenia, które nie kończą się, mam wrażenie, że określenie rozmiaru zestawu rozwiązań może być równoznaczne z rozwiązaniem problemu zatrzymania, ale nie jestem całkowicie pewien ...)
Co się stanie, jeśli jedno zlecenie redukcji nie zakończy się, a drugie nie? Czy otrzymujesz zakończenie? – augustss
Aha, a twoja implementacja SKI jest wystarczającym dowodem na to, że Turing jest kompletny. – augustss
@augustss Ostrożnie zaaranżowałem, że kod próbuje normalnej redukcji rzędu _first_. Więc jeśli istnieje normalna forma, znajdzie się ona w skończonej pozycji w zestawie rozwiązań. Jeśli jednak istnieje niekończąca się kolejność redukcji, soler ma gwarancję, że ją znajdzie i wygeneruje nieskończony zestaw rozwiązań.Tworzy nieskończony zestaw, który zawiera prawidłową odpowiedź, wystarczającą do osiągnięcia Turinga? Chodzi mi o to, że wyliczenie wszystkich możliwych wyrażeń SKI mogłoby to zrobić ... – MathematicalOrchid