Napisz wyrażenie matematyczne, używając symboli:
There exists at least one non-negative integer
(zapisany jakoE
, egzystencjalny kwantyfikator)All non-negative integers
(zapisany jakoA
uniwersalny kwantyfikator)+
(dodanie)*
(mnożenie)=
(równość)>
,<
(operatory porównania)&
(i),|
(lub),!
(nie)(
,)
(do grupowania)- nazwy zmiennych
co jest równoważne z instrukcją
Istnieje liczba wymierna a, taka że π + e * a jest wymierna.
(oczywiście to stała matematyczna równa obwodowi podzielonemu przez średnicę koła, zaś to liczba Eulera )
Musisz udowodnić, że twoje oświadczenie jest rzeczywiście równoważne powyższemu oświadczeniu.
Oczywiście „najkrótszą” drogą do tego jest udowodnienie twierdzenia prawdziwego lub fałszywego, a następnie udzielenie odpowiedzi trywialnie prawdziwym lub fałszywym, ponieważ wszystkie prawdziwe stwierdzenia są sobie równe, podobnie jak wszystkie fałszywe stwierdzenia.
Jednak wartość prawdziwości danego stwierdzenia jest nierozwiązanym problemem w matematyce : nawet nie wiemy, czy jest irracjonalne! Dlatego, z wyjątkiem przełomowych badań matematycznych, wyzwaniem jest znalezienie „prostej” równoważnej instrukcji, udowodnienie jej równoważności i opisanie jej jak najkrócej.
Punktacja
E
A
+
*
=
>
<
&
|
i !
każdy dodaje 1 do wyniku. (
i )
nie dodawaj niczego do wyniku. Każda nazwa zmiennej dodaje 1 do wyniku.
Np. E x (A ba x+ba>x*(x+ba))
Wynik 13 ( E
x
A
ba
x
+
ba
>
x
*
x
+
ba
)
Najniższy wynik wygrywa.
Uwaga:
Oświadczenie: Ta notatka nie została napisana przez OP.
- To nie jest wyzwanie do gry w golfa . Odpowiedzi nie muszą zawierać kodu.
- Jest to podobne do wyzwania w golfa , ale nie takie , ponieważ musisz napisać oświadczenie i udowodnić, że jest ono równoważne z innym stwierdzeniem.
- Możesz przesłać trywialnie prawdziwe (np. Dla wszystkich x, x = x
Ax x=x
) lub trywialnie fałszywe oświadczenie (np. Dla wszystkich x, x> xAx x>x
), jeśli możesz udowodnić, że powyższe stwierdzenie jest prawdziwe / fałszywe. - Możesz używać dodatkowych symboli (podobnych do lematu w proof-golfie), ale wynik będzie liczony tak samo, jak ich nie użyjesz.
Na przykład, jeśli zdefiniujesz,a => b
że znaczysz(!a) | b
, za każdym razem, gdy użyjesz=>
dowodu, twój wynik wzrasta o 2. Ponieważ stałych nie ma na liście w dozwolonych symbolach, nie wolno ich używać.
Na przykład: Instrukcja1 > 0
może być zapisana jakoForall zero: ( zero + zero = zero ) => Forall one: ( Forall x: x * one = x ) => one > zero
przy wyniku 23. (pamiętaj, że
=>
kosztuje 2 za użycie).
Poradnik
- Aby użyć stałych naturalnych, możesz to zrobić
E0, 0+0=0 & E1, At 1*t=t &
(więc nie potrzebujesz,=>
co jest bardziej ekspansywne); dla liczb większych niż 1, wystarczy dodać 1
You are allowed to submit a trivially-true (e.g., for all x, x = x Ax x=x) or a trivially-false statement (e.g., for all x, x > x Ax x>x) if you can prove the statement above is true/false.
. Oświadczenie nie jest teraz ani udowodnione, ani obalone, więc naprawdę nie mam nic przeciwko, jeśli problem się nudzi, ponieważ taki problem został rozwiązanyI'd be impressed by any solution no matter the score.
Wynik był tylko cel dla tych, którzy mogą rozwiązać ten problemOdpowiedzi:
671
E a (a+a>a*a & (E b (E c (E d (A e (A f (f<a | (E g (E h (E i ((A j ((!(j=(f+f+h)*(f+f+h)+h | j=(f+f+a+i)*(f+f+a+i)+i) | j+a<e & (E k ((A l (!(l>a & (E m k=l*m)) | (E m l=e*m))) & (E l (E m (m<k & g=(e*l+(j+a))*k+m)))))) & (A k (!(E l (l=(j+k)*(j+k)+k+a & l<e & (E m ((A n (!(n>a & (E o m=n*o)) | (E o n=e*o))) & (E n (E o (o<m & g=(e*n+l)*m+o))))))) | j<a+a & k=a | (E l (E m ((E n (n=(l+m)*(l+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & g=(e*p+n)*o+q))))))) & j=l+a+a & k=j*j*m))))))) & (E j (E k (E l ((E m (m=(k+l)*(k+l)+l & (E n (n=(f+m)*(f+m)+m+a & n<e & (E o ((A p (!(p>a & (E q o=p*q)) | (E q p=e*q))) & (E p (E q (q<o & j=(e*p+n)*o+q))))))))) & (A m (A n (A o (!(E p (p=(n+o)*(n+o)+o & (E q (q=(m+p)*(m+p)+p+a & q<e & (E r ((A s (!(s>a & (E t r=s*t)) | (E t s=e*t))) & (E s (E t (t<r & j=(e*s+q)*r+t))))))))) | m<a & n=a & o=f | (E p (E q (E r (!(E s (s=(q+r)*(q+r)+r & (E t (t=(p+s)*(p+s)+s+a & t<e & (E u ((A v (!(v>a & (E w u=v*w)) | (E w v=e*w))) & (E v (E w (w<u & j=(e*v+t)*u+w))))))))) | m=p+a & n=(f+a)*q & o=f*r)))))))) & (E m (m=b*(h*f)*l & (E n (n=b*(h*f+h)*l & (E o (o=c*(k*f)*i & (E p (p=c*(k*f+k)*i & (E q (q=d*i*l & (m+o<q & n+p>q | m<p+q & n>o+q | o<n+q & p>m+q))))))))))))))))))))))))))
Jak to działa
Najpierw pomnóż przez rzekome wspólne mianowniki a i (π + e · a), aby przepisać warunek jako: istnieje a, b, c ∈ ℕ (nie wszystkie zero) z · π + b · e = c lub a · π - b · e = c lub −a · π + b · e = c. Do rozwiązania problemów ze znakami potrzebne są trzy przypadki.
Następnie musimy przepisać to, aby mówić o π i e poprzez racjonalne aproksymacje: dla wszystkich racjonalnych aproksymacji π₀ <π <π₁ i e₀ <e <e₁, mamy · π₀ + b · e₀ <c <a · π₁ + b · e₁ lub a π₀ - b · e₁ <c <a · π₁ + b · e₀ lub −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Pamiętaj, że otrzymujemy teraz warunek „nie wszystkie zero”).
Teraz najtrudniejsza część. Jak uzyskać te racjonalne przybliżenia? Chcemy używać formuł takich jak
2/1 · 2/3 · 4/3 · 4/5 ⋯ (2 · k) / (2 · k + 1) <π / 2 <2/1 · 2/3 · 4/3 · 4/5 ⋯ (2 · k) / (2 · k + 1) · (2 · k + 2) / (2 · k + 1),
((k + 1) / k) k <e <((k + 1) / k) k + 1 ,
ale nie ma oczywistego sposobu na napisanie iteracyjnych definicji tych produktów. Więc zbudowaliśmy trochę maszyn, które po raz pierwszy opisałem w tym poście Quora . Zdefiniuj:
dzieli (d, a): = ∃b, a = d · b,
powerOfPrime (a, p): = ∀b, ((b> 1 i dzieli (b, a)) ⇒ dzieli (p, b)),
który jest spełniony, jeśli aff = 1 lub p = 1, lub p jest liczbą pierwszą, a a jest jego siłą. Następnie
isDigit (a, s, p): = a <p i ∃b, (powerOfPrime (b, p) i ∃qr, (r <b i s = (p · q + a) · b + r))
jest spełnione iff a = 0, lub a jest cyfrą podstawowej liczby s. To pozwala nam reprezentować dowolny zbiór skończony za pomocą cyfr jakiegoś podstawowego numeru p. Teraz możemy przetłumaczyć obliczenia iteracyjne pisząc, z grubsza istnieje zbiór stanów pośrednich, tak że stan końcowy znajduje się w zbiorze, a każdy stan w zbiorze jest stanem początkowym lub następuje w jednym kroku od innego stanu w zbiorze zestaw.
Szczegóły znajdują się w kodzie poniżej.
Generowanie kodu w Haskell
Wypróbuj online!
źródło
isDigit
, jedyne miejsce, w którym go używasz.powerOfPrime
iisDigit
skończyć reprezentujący w nieprzewidzianych przypadkach, o ile istnieje jakiś sposób, aby reprezentować każdy skończony zbiór.)a
ma 7 lub więcej punktów, myślę, że warto dodaćex (\a' -> a' := a :& ... )
opakowanieisDigit
.k>0
, ponieważeBound
daje zerowy mianownik (i jeden zerowy licznik) w tejk==0
sprawie, więc wszystkie alternatywy zawodzą.270
a|b&c
jest,a|(b&c)
ponieważ myślę, że usunięcie tych nawiasów sprawia, że wyglądają lepiej, w każdym razie są one bezpłatne.Używa JavaScript
"(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)
do liczenia tokenów.źródło
mult = t
? Ponadto, ponieważx
może mieć tylko skończoną liczbę cyfr, musisz pozwoliće1 = e2 = 0
na wystarczająco dużet
. Będziesz także potrzebować więcej nawiasów lub innych niedwuznaczności dla niejednoznacznych konstrukcji, takich jak_ & _ | _
.mult
. Nie widzę żadnego problemumult=t2
na końcu.e1=e2=0
powinien zostać naprawiony, ale nie tak pewny, więc obecnie nie zmieniam akceptacji.a & b | c
jest(a & b) | c
to twójt*1=t
jest zdecydowanie w złym miejscu. Nie wykluczyłeś też trywialnego rozwiązaniac1 = c4 & c2 = c5 & c3 = 0 & diff = diff2
.diff≠diff2
pracować?!(c2=c5)
jak już wiemy,e
jest irracjonalny, więc nawet jeśli to nie zadziała, wynik nie wzrośnie