Ta odpowiedź jest formalnym dowodem na odpowiedź przez TheNumberOne , Wyliczanie ważny Brainf ** k programów , w których może to być trochę trudne do zrozumienia punktów drobne dlaczego wyliczenie jest prawidłowe. Nie jest łatwo zrozumieć, dlaczego nie ma żadnego nieprawidłowego programu, który mapuje na liczbę nieobjętą prawidłowym programem.
W tej odpowiedzi wielkie litery są używane do oznaczenia programów, a zmienne pisane małymi literami są używane dla funkcji i liczb całkowitych. ~ jest operatorem konkatenacji.
Twierdzenie 1:
Niech funkcja f będzie programem opisanym w tej odpowiedzi. Następnie dla każdego programu U istnieje poprawny program V taki, że f (U) = f (V)
Definicja 1:
Niech g (X) będzie liczbą, [
która pojawi się w programie X, i niech h (X) będzie liczbą, ]
która pojawi się.
Definicja 2:
Zdefiniuj P (x) jako tę funkcję:
P(x) = "" (the empty program) when x <= 0
P(x) = "]" when x = 1
P(x) = "]]" when x = 2
etcetera
Definicja 3:
Biorąc pod uwagę program X, oznacz X1 jako największy prefiks [
znaków, X2 jego środek, a X3 jego największy sufiks ]
znaków.
Dowód propozycji 1:
Jeśli g (U) = h (U), to U jest poprawnym programem i możemy przyjąć V = U. (trywialny przypadek).
Jeśli g (U) <h (U), możemy stworzyć V, poprzedzając symbole n = h (U) - g (U) [
. Oczywiście f (V) = f (U), ponieważ wszystkie [
symbole w prefiksie są usuwane.
Teraz rozważ g (U)> h (U). Zdefiniuj T = U2 ~ U3. jeśli g (T) <= h (T), to możemy zbudować V usuwając [
symbole n = g (U) - h (U) .
Możemy więc założyć, że h (T) <g (T). Konstruuj V = T ~ P (g (T) - h (T)).
Potrzebujemy trzech drobnych faktów:
Zastrzeżenie 1: g (U2) = g (T)
U3 [
z definicji nie zawiera żadnych symboli. Ponieważ T = U2 ~ U3, wszystkie jego [
symbole znajdują się w pierwszej części.
Twierdzenie 2: h (U3) <g (T)
Wynika to z faktu, że h (T) <g (T) i h (U3) <h (U3 ~ U2) = h (T).
Twierdzenie 3: h (V3) = g (U2) - h (U2)
h(V3) = h(U3) + g(T) - h(T) using the construction of V
h(V3) = h(U3) + g(U2) + g(U3) - h(U2) - h(U3) apply the definition of T
h(V3) = g(U2) - h(U2) *one term cancels, g(U3) is always zero, as U3 contains only `]` symbols*
Teraz pokazujemy, że f (V) = f (U).
f(U) = U2 ~ P(h(U3) - g(U2)) = U2 claim 2, definition of P
f(V) = U2 ~ P(h(V3) - g(V2))
= U2 ~ P(h(V3) - g(U2))
= U2 ~ P(g(U2) - h(U2) - g(U2)) claim 3
= U2 ~ P(-h(U2))
= U2 definition P
To kończy dowód. CO BYŁO DO OKAZANIA
Zróbmy także wyjątkowość.
Twierdzenie 2:
Niech U, V będą dwoma różnymi, poprawnymi programami. Następnie f (U)! = F (V)
Jest to dość proste w porównaniu z poprzednią propozycją.
Załóżmy, że U2 = V2. Ale wtedy jedynym sposobem, w jaki U i V mogą być różne, jest dodanie lub usunięcie n [
i ]
symboli odpowiednio do U1 i U3. Zmienia to jednak wynik f, ponieważ f policzy liczbę niedopasowanych ]
symboli w sufiksie.
Zatem U2! = V2.
Oczywiście prowadzi to do sprzeczności. Ponieważ U2 i V2 są dosłownie zawarte w danych wyjściowych odpowiednio f (U) i f (V), nie mogą się różnić, z wyjątkiem „krawędzi” miejsca, w którym U2 jest połączone z U3. Ale pierwszy i ostatni symbol U2 i V2 nie mogą być [
lub ]
z definicji, podczas gdy są to jedyne symbole dozwolone odpowiednio w U1, U3, V1, V3 i odpowiednio. Otrzymujemy U2 = V2. CO BYŁO DO OKAZANIA