Escreva uma declaração matemática, usando os símbolos:
There exists at least one non-negative integer
(escrito comoE
quantificador existencial)All non-negative integers
(escrito comoA
quantificador universal)+
(Adição)*
(multiplicação)=
(igualdade)>
,<
(operadores de comparação)&
(e),|
(ou),!
(não)(
,)
(para agrupar)- nomes de variáveis
que é equivalente à declaração
Existe um número racional a, de modo que π + e * a é racional.
(é claro, é a constante matemática igual à circunferência dividida pelo diâmetro de um círculo e é o número de Euler )
Você deve provar que sua afirmação é realmente equivalente à afirmação acima.
Obviamente, o caminho "mais curto" para fazer isso é provar a afirmação verdadeira ou falsa e, em seguida, responder com uma afirmação trivialmente verdadeira ou falsa, pois todas as afirmações verdadeiras são equivalentes entre si, assim como todas as afirmações falsas.
No entanto, o valor de verdade da afirmação dada é um problema não resolvido em matemática : nem sabemos se é irracional! Portanto, impedindo a pesquisa matemática inovadora, o desafio é encontrar uma declaração equivalente "simples", provar sua equivalência e descrevê-la o mais brevemente possível.
Pontuação
E
A
+
*
=
>
<
&
|
e !
cada um adiciona 1 à pontuação. (
e )
não adicione nada à pontuação. Cada nome de variável adiciona 1 à pontuação.
Por exemplo, E x (A ba x+ba>x*(x+ba))
pontuação 13 ( E
x
A
ba
x
+
ba
>
x
*
x
+
ba
)
Menor pontuação ganha.
Nota:
Isenção de responsabilidade: Esta nota não foi escrita pelo OP.
- Este não é um desafio do código-golfe . As respostas não são necessárias para conter o código.
- Isso é semelhante, mas não é, um desafio à prova de golfe , pois você precisa escrever uma declaração e provar que é equivalente a outra declaração.
- Você tem permissão para enviar uma
Ax x=x
declaração trivialmente verdadeira (por exemplo, para todos os x, x = x ) ou uma declaração trivialmente falsa (por exemplo, para todos os x, x> xAx x>x
) se puder provar que a declaração acima é verdadeira / falsa. - Você tem permissão para usar símbolos adicionais (semelhante ao lema no golfe de prova), mas a pontuação será contada da mesma forma que você não os usa.
Por exemplo, se você definira => b
como significante(!a) | b
, cada vez que usar=>
sua prova, sua pontuação aumentará 2. Como as constantes não estão listadas nos símbolos permitidos, você não deve usá-las.
Por exemplo: A declaração1 > 0
pode ser escrita comoForall zero: ( zero + zero = zero ) => Forall one: ( Forall x: x * one = x ) => one > zero
na pontuação de 23. (lembre-se de que
=>
custa 2 por uso).
Dicas
- Para usar constantes naturais, você pode fazer
E0, 0+0=0 & E1, At 1*t=t &
(para não precisar do=>
que é mais expansivo); para números maiores que 1, adicione alguns 1's
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.
. A declaração está agora provado nem refutado, então eu realmente não me importo se o problema fica chato porque tal problema está resolvidoI'd be impressed by any solution no matter the score.
A pontuação foi apenas para apontar para aqueles que podem resolver este problemaRespostas:
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))))))))))))))))))))))))))
Como funciona
Primeiro, multiplique pelos denominadores comuns supostos de a e (π + e · a) para reescrever a condição como: existe a, b, c ∈ ℕ (nem todo zero) com a · π + b · e = c ou a · π - b · e = c ou −a · π + b · e = c. Três casos são necessários para lidar com problemas de sinal.
Então, precisamos reescrever isso para falar sobre π e e por aproximações racionais: para todas as aproximações racionais π₀ <π <π₁ e e₀ <e <e₁, temos a · π₀ + b · e₀ <c <a · π₁ + b · e₁ ou a · π₀ - b · e₁ <c <a · π₁ + b · e₀ ou −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Observe que agora obtemos a condição "nem todo zero" de graça.)
Agora, para a parte difícil. Como obtemos essas aproximações racionais? 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 ,
mas não há maneira óbvia de escrever as definições iterativas desses produtos. Então, construímos um pouco de maquinaria que descrevi pela primeira vez neste post do Quora . Definir:
divide (d, a): = ∃b, a = d · b,
powerOfPrime (a, p): = ∀b, ((b> 1 e divide (b, a)) ⇒ divide (p, b)),
que é satisfeito se a = 1, ou p = 1, ou p é primo e a é um poder disso. Então
isDigit (a, s, p): = a <p e ∃b, (powerOfPrime (b, p) e ∃qr, (r <be s = (p · q + a) · b + r))
é satisfeito se a = 0 ou a é um dígito do número da base-p s. Isso nos permite representar qualquer conjunto finito usando os dígitos de algum número base-p. Agora, podemos traduzir cálculos iterativos escrevendo, aproximadamente, que existe um conjunto de estados intermediários, de modo que o estado final está no conjunto, e cada estado no conjunto é o estado inicial ou segue em uma etapa de outro estado no conjunto.
Os detalhes estão no código abaixo.
Gerando código no Haskell
Experimente online!
fonte
isDigit
, o único local em que você o usa.powerOfPrime
eisDigit
acabam representando em casos inesperados, desde que haja alguma forma de representar cada conjunto finito.)a
tiver pontuação 7 ou superior, acho, vale a pena adicionar umex (\a' -> a' := a :& ... )
invólucroisDigit
.k>0
, poiseBound
fornece um denominador zero (e um numerador zero) nok==0
caso, então todas as alternativas falham.270
a|b&c
éa|(b&c)
porque acho que remover esses parênteses faz com que pareça melhor, de qualquer maneira eles são gratuitos.Utilizou JavaScript
"(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)
para contar tokens.fonte
mult = t
? Além disso, comox
só pode ter muitos dígitos finitos, você precisará permitire1 = e2 = 0
que sejam suficientemente grandest
. Além disso, você precisará de mais parênteses ou outra desambiguação para construções ambíguas, como_ & _ | _
.mult
. Não vejo nenhum problemamult=t2
no final.e1=e2=0
deve ser corrigido, mas não tão certo, então, atualmente, não mudo a aceitação.a & b | c
for,(a & b) | c
então vocêt*1=t
está definitivamente no lugar errado. Além disso, você não excluiu a solução trivialc1 = c4 & c2 = c5 & c3 = 0 & diff = diff2
.diff≠diff2
trabalhar?!(c2=c5)
como já sabemos quee
é irracional, portanto, mesmo que isso não funcione, a pontuação não aumentará