Escribe una declaración matemática, usando los símbolos:
There exists at least one non-negative integer
(escrito comoE
cuantificador existencial)All non-negative integers
(escrito comoA
cuantificador universal)+
(adición)*
(multiplicación)=
(igualdad)>
,<
(operadores de comparación)&
(y),|
(o),!
(no)(
,)
(para agrupar)- nombres de variables
que es equivalente a la declaración
Existe un número racional a, tal que π + e * a es racional.
(por supuesto, es la constante matemática igual a la circunferencia dividida por el diámetro de un círculo, y es el número de Euler )
Debe probar que su declaración es de hecho equivalente a la declaración anterior.
Obviamente, la forma "más corta" de hacerlo es probar que la afirmación es verdadera o falsa, y luego responder con una declaración trivialmente verdadera o falsa, ya que todas las declaraciones verdaderas son equivalentes entre sí, al igual que todas las declaraciones falsas.
Sin embargo, el valor de verdad de la declaración dada es un problema no resuelto en matemáticas : ¡ni siquiera sabemos si es irracional! Por lo tanto, salvo la investigación matemática innovadora, el desafío es encontrar una declaración equivalente "simple", demostrar su equivalencia y describirla lo más brevemente posible.
Puntuación
E
A
+
*
=
>
<
&
|
y !
cada uno agrega 1 al puntaje. (
y )
no agregue nada al puntaje. Cada nombre de variable agrega 1 al puntaje.
Por ejemplo, E x (A ba x+ba>x*(x+ba))
puntaje 13 ( E
x
A
ba
x
+
ba
>
x
*
x
+
ba
)
La puntuación más baja gana.
Nota:
Descargo de responsabilidad: esta nota no fue escrita por el OP.
- Este no es un desafío de código de golf . No se requiere que las respuestas contengan código.
- Esto es similar, pero no, un desafío de prueba de golf , ya que necesita escribir una declaración y demostrar que es equivalente a otra declaración.
- Puede enviar una
Ax x=x
declaración trivialmente verdadera (por ejemplo, para todas las x, x = x ) o una declaración trivialmente falsa (por ejemplo, para todas las x, x> xAx x>x
) si puede probar que la declaración anterior es verdadera / falsa. - Se le permite usar símbolos adicionales (similares al lema en prueba de golf), pero el puntaje se contará de la misma manera que no los usa.
Por ejemplo, si definea => b
que significa(!a) | b
, cada vez que usa=>
en su prueba, su puntaje aumenta en 2. Debido a que las constantes no figuran en los símbolos permitidos, no debe usarlas.
Por ejemplo: la declaración1 > 0
se puede escribir comoForall zero: ( zero + zero = zero ) => Forall one: ( Forall x: x * one = x ) => one > zero
con un puntaje de 23. (recuerde que
=>
cuesta 2 por uso).
Consejos
- Para usar constantes naturales, puede hacerlo
E0, 0+0=0 & E1, At 1*t=t &
(por lo que no necesita=>
cuál es más expansivo); para números mayores que 1, solo agregue algunos 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.
. La declaración ahora no está probada ni refutada, así que realmente no me importa si el problema se vuelve aburrido porque tal problema está resueltoI'd be impressed by any solution no matter the score.
El puntaje fue solo para apuntar a aquellos que pueden resolver este problemaRespuestas:
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))))))))))))))))))))))))))
Cómo funciona
Primero, multiplíquelo por los supuestos denominadores comunes de a y (π + e · a) para reescribir la condición como: existen a, b, c ∈ ℕ (no todos cero) con a · π + b · e = c o a · π - b · e = c o −a · π + b · e = c. Son necesarios tres casos para tratar los problemas de signos.
Luego, tendremos que reescribir esto para hablar sobre π y e mediante aproximaciones racionales: para todas las aproximaciones racionales π₀ <π <π₁ y e₀ <e <e₁, tenemos a · π₀ + b · e₀ <c <a · π₁ + b · e₁ o a · π₀ - b · e₁ <c <a · π₁ + b · e₀ o −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Tenga en cuenta que ahora obtenemos la condición "no todo cero" de forma gratuita).
Ahora para la parte difícil. ¿Cómo obtenemos estas aproximaciones racionales? Queremos usar fórmulas como
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 ,
pero no hay una forma obvia de escribir las definiciones iterativas de estos productos. Así que construimos un poco de maquinaria que describí por primera vez en esta publicación de Quora . Definir:
divide (d, a): = ∃b, a = d · b,
powerOfPrime (a, p): = ∀b, ((b> 1 y divide (b, a)) ⇒ divide (p, b)),
que se satisface si a = 1, o p = 1, o p es primo y a es una potencia de él. Luego
isDigit (a, s, p): = a <p y ∃b, (powerOfPrime (b, p) y ∃qr, (r <b y s = (p · q + a) · b + r))
se satisface si a = 0, o a es un dígito del número base-p s. Esto nos permite representar cualquier conjunto finito utilizando los dígitos de algún número base-p. Ahora podemos traducir cálculos iterativos al escribir, aproximadamente, existe un conjunto de estados intermedios de tal manera que el estado final está en el conjunto, y cada estado en el conjunto es el estado inicial o sigue en un paso desde algún otro estado en el conjunto.
Los detalles están en el código a continuación.
Generando código en Haskell
Pruébalo en línea!
fuente
isDigit
, el único lugar donde lo usa.powerOfPrime
yisDigit
terminen representando en casos inesperados, siempre que haya alguna forma de representar cada conjunto finito).a
tiene una puntuación de 7 o superior, creo, entonces valdrá la pena agregar unex (\a' -> a' := a :& ... )
contenedorisDigit
.k>0
, ya queeBound
da un denominador cero (y un numerador cero) en elk==0
caso, por lo que todas las alternativas fallan.270
a|b&c
esa|(b&c)
porque creo que eliminar estos paréntesis hace que se vea mejor, de todos modos son gratuitos.Se utilizó JavaScript
"(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)
para contar tokens.fuente
mult = t
? Además, dadox
que solo puede tener un número finito de dígitos, deberá tener en cuenta loe1 = e2 = 0
suficientemente grandet
. También necesitará más paréntesis u otra desambiguación para construcciones ambiguas como_ & _ | _
.mult
. No veo ningún problemamult=t2
al final.e1=e2=0
debería arreglarse pero no es tan cierto, por lo que actualmente no cambio la aceptación.a & b | c
es(a & b) | c
así,t*1=t
definitivamente está en el lugar equivocado. Además, no ha excluido la solución trivialc1 = c4 & c2 = c5 & c3 = 0 & diff = diff2
.diff≠diff2
funciona?!(c2=c5)
como ya sabemos,e
es irracional, por lo que incluso si esto no funciona, el puntaje no aumentará