Escríbelo en el estilo de teoría de números

19

Escribe una declaración matemática, usando los símbolos:

  • There exists at least one non-negative integer(escrito como Ecuantificador existencial)
  • All non-negative integers(escrito como Acuantificador 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, π=3.1415 ... es la constante matemática igual a la circunferencia dividida por el diámetro de un círculo, y mi=2.7182 ... 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 π+mi 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 . No se requiere que las respuestas contengan código.
  • Esto es similar, pero no, un desafío de , ya que necesita escribir una declaración y demostrar que es equivalente a otra declaración.
  • Puede enviar una Ax x=xdeclaración trivialmente verdadera (por ejemplo, para todas las x, x = x ) o una declaración trivialmente falsa (por ejemplo, para todas las x, x> x Ax 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 define a => bque 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ón 1 > 0se puede escribir como

    
    Forall 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
l4m2
fuente
55
Me gusta el concepto aquí, pero la declaración es realmente difícil de escribir y me impresionaría cualquier solución sin importar el puntaje. Hubiera sugerido usar algo más simple para que más personas participen.
xnor
1
Necesita una declaración matemática que sea equivalente a la dada. ¿En qué sentido deberían ser equivalentes ? Si estoy en lo correcto, la declaración dada es falsa. Entonces, su equivalencia con otras declaraciones es difícil para mí. Por ejemplo, ¿es equivalente a Existe un número racional a, tal que i + e * a es racional (donde i es la unidad imaginaria)?
Luis Mendo
1
Nota actual solo decir 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á resuelto
l4m2
1
La pregunta, tal como está escrita, pareció enterrar principalmente al lede y evitar explicar lo que realmente está sucediendo, así que escribí una pequeña explicación en las notas (que la no trivialidad del desafío depende del valor de verdad actualmente desconocido de la declaración dada) .
Lynn
I'd be impressed by any solution no matter the score.El puntaje fue solo para apuntar a aquellos que pueden resolver este problema
l4m2

Respuestas:

27

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

{-# LANGUAGE ImplicitParams, TypeFamilies, Rank2Types #-}

-- Define an embedded domain-specific language for propositions.
infixr 2 :|

infixr 3 :&

infix 4 :=

infix 4 :>

infix 4 :<

infixl 6 :+

infixl 7 :*

data Nat v
  = Var v
  | Nat v :+ Nat v
  | Nat v :* Nat v

instance Num (Nat v) where
  (+) = (:+)
  (*) = (:*)
  abs = id
  signum = error "signum Nat"
  fromInteger = error "fromInteger Nat"
  negate = error "negate Nat"

data Prop v
  = Ex (v -> Prop v)
  | Al (v -> Prop v)
  | Nat v := Nat v
  | Nat v :> Nat v
  | Nat v :< Nat v
  | Prop v :& Prop v
  | Prop v :| Prop v
  | Not (Prop v)

-- Display propositions in the given format.
allVars :: [String]
allVars = do
  s <- "" : allVars
  c <- ['a' .. 'z']
  pure (s ++ [c])

showNat :: Int -> Nat String -> ShowS
showNat _ (Var v) = showString v
showNat prec (a :+ b) =
  showParen (prec > 6) $ showNat 6 a . showString "+" . showNat 7 b
showNat prec (a :* b) =
  showParen (prec > 7) $ showNat 7 a . showString "*" . showNat 8 b

showProp :: Int -> Prop String -> [String] -> ShowS
showProp prec (Ex p) (v:free) =
  showParen (prec > 1) $ showString ("E " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (Al p) (v:free) =
  showParen (prec > 1) $ showString ("A " ++ v ++ " ") . showProp 4 (p v) free
showProp prec (a := b) _ =
  showParen (prec > 4) $ showNat 5 a . showString "=" . showNat 5 b
showProp prec (a :> b) _ =
  showParen (prec > 4) $ showNat 5 a . showString ">" . showNat 5 b
showProp prec (a :< b) _ =
  showParen (prec > 4) $ showNat 5 a . showString "<" . showNat 5 b
showProp prec (p :& q) free =
  showParen (prec > 3) $
  showProp 4 p free . showString " & " . showProp 3 q free
showProp prec (p :| q) free =
  showParen (prec > 2) $
  showProp 3 p free . showString " | " . showProp 2 q free
showProp _ (Not p) free = showString "!" . showProp 9 p free

-- Compute the score.
scoreNat :: Nat v -> Int
scoreNat (Var _) = 1
scoreNat (a :+ b) = scoreNat a + 1 + scoreNat b
scoreNat (a :* b) = scoreNat a + 1 + scoreNat b

scoreProp :: Prop () -> Int
scoreProp (Ex p) = 2 + scoreProp (p ())
scoreProp (Al p) = 2 + scoreProp (p ())
scoreProp (p := q) = scoreNat p + 1 + scoreNat q
scoreProp (p :> q) = scoreNat p + 1 + scoreNat q
scoreProp (p :< q) = scoreNat p + 1 + scoreNat q
scoreProp (p :& q) = scoreProp p + 1 + scoreProp q
scoreProp (p :| q) = scoreProp p + 1 + scoreProp q
scoreProp (Not p) = 1 + scoreProp p

-- Convenience wrappers for n-ary exists and forall.
class OpenProp p where
  type OpenPropV p
  ex, al :: p -> Prop (OpenPropV p)

instance OpenProp (Prop v) where
  type OpenPropV (Prop v) = v
  ex = id
  al = id

instance (OpenProp p, a ~ Nat (OpenPropV p)) => OpenProp (a -> p) where
  type OpenPropV (a -> p) = OpenPropV p
  ex p = Ex (ex . p . Var)
  al p = Al (al . p . Var)

-- Utility for common subexpression elimination.
cse :: Int -> Nat v -> (Nat v -> Prop v) -> Prop v
cse uses x cont
  | (scoreNat x - 1) * (uses - 1) > 6 = ex (\x' -> x' := x :& cont x')
  | otherwise = cont x

-- p implies q.
infixl 1 ==>

p ==> q = Not p :| q

-- Define one as the unique n with n+n>n*n.
withOne ::
     ((?one :: Nat v) =>
        Prop v)
  -> Prop v
withOne p =
  ex
    (\one ->
       let ?one = one
       in one + one :> one * one :& p)

-- a is a multiple of d.
divides d a = ex (\b -> a := d * b)

-- a is a power of p (assuming p is prime).
powerOfPrime a p = al (\b -> b :> ?one :& divides b a ==> divides p b)

-- a is 0 or a digit of the base-p number s (assuming p is prime).
isDigit a s p =
  cse 2 a $ \a ->
    a :< p :&
    ex
      (\b -> powerOfPrime b p :& ex (\q r -> r :< b :& s := (p * q + a) * b + r))

-- An injection from ℕ² to ℕ, for representing tuples.
pair a b = (a + b) ^ 2 + b

-- πn₀/πd < π/4 < πn₁/πd, with both fractions approaching π/4 as k
-- increases:
-- πn₀ = 2²·4²·6²⋯(2·k)²·k
-- πn₁ = 2²·4²·6²⋯(2·k)²·(k + 1)
-- πd = 1²⋅3²·5²⋯(2·k + 1)²
πBound p k cont =
  ex
    (\s x πd ->
       al
         (\i ->
            (i := pair (k + k) x :| i := pair (k + k + ?one) πd ==>
             isDigit (i + ?one) s p) :&
            al
              (\a ->
                 isDigit (pair i a + ?one) s p ==>
                 ((i :< ?one + ?one :& a := ?one) :|
                  ex
                    (\i' a' ->
                       isDigit (pair i' a' + ?one) s p :&
                       i := i' + ?one + ?one :& a := i ^ 2 * a')))) :&
       let πn = x * k
           πn = πn + x
       in cont πn πn πd)

-- en₀/ed < e < en₁/ed, with both fractions approaching e as k
-- increases:
-- en₀ = (k + 1)^k * k
-- en₁ = (k + 1)^(k + 1)
-- ed = k^(k + 1)
eBound p k cont =
  ex
    (\s x ed ->
       cse 3 (pair x ed) (\y -> isDigit (pair k y + ?one) s p) :&
       al
         (\i a b ->
            cse 3 (pair a b) (\y -> isDigit (pair i y + ?one) s p) ==>
            (i :< ?one :& a := ?one :& b := k) :|
            ex
              (\i' a' b' ->
                 cse 3 (pair a' b') (\y -> isDigit (pair i' y + ?one) s p) ==>
                 i := i' + ?one :& a := (k + ?one) * a' :& b := k * b')) :&
       let en = x * k
           en = en + x
       in cont en en ed)

-- There exist a, b, c ∈ ℕ (not all zero) with a·π/4 + b·e = c or
-- a·π/4 = b·e + c or b·e = a·π/4 + c.
prop :: Prop v
prop =
  withOne $
  ex
    (\a b c ->
       al
         (\p k ->
            k :< ?one :|
            Bound p k $ n πn πd ->
               eBound p k $ \en en ed ->
                 cse 3 (a * πn * ed) $ \x ->
                   cse 3 (a * πn * ed) $ \x ->
                     cse 3 (b * en * πd) $ \y ->
                       cse 3 (b * en * πd) $ \y ->
                         cse 6 (c * πd * ed) $ \z ->
                           (x + y :< z :& x + y :> z) :|
                           (x :< y + z :& x :> y + z) :|
                           (y :< x + z :& y :> x + z))))

main :: IO ()
main = do
  print (scoreProp prop)
  putStrLn (showProp 0 prop allVars "")

Pruébalo en línea!

Anders Kaseorg
fuente
"que se satisface si f a = 1, o p es primo y a es una potencia de él" - también puede tener p = 1. Aunque p> 1 está implícito en isDigit, el único lugar donde lo usa.
Ørjan Johansen
@ ØrjanJohansen Gracias, arreglé esa nota. (En realidad, no importa qué conjuntos powerOfPrimey isDigitterminen representando en casos inesperados, siempre que haya alguna forma de representar cada conjunto finito).
Anders Kaseorg
2
Si atiene una puntuación de 7 o superior, creo, entonces valdrá la pena agregar un ex (\a' -> a' := a :& ... )contenedor isDigit.
Ørjan Johansen el
@ ØrjanJohansen Claro, eso ahorra 68. ¡Gracias!
Anders Kaseorg el
Creo que debe requerir k>0, ya que eBoundda un denominador cero (y un numerador cero) en el k==0caso, por lo que todas las alternativas fallan.
Ørjan Johansen el
3

270

E1                                                                              { Exist 1, defined when Any k introduced }
Ec1 Ec2 Ec3 Ec4 Ec5 Ak k*1=k & c3>1 & ( En0 An n<n0 |                           { for large enough n, |(c1-c4)e+c3(4-pi)/8+(c2-c5)|<1/k }
Ex Ep Ew Emult At (Eb ((b>1 & Eh b*h=t) &! Eh h*p=b)) |                         { x read in base-p, then each digit in base-w. t as a digit }
Ee1 Ee2 Ehigher Elower e2<p & lower<t & ((higher*p+e1)*p+e2)*t+lower=x &        { last digit e1, this digit e2 }
    { Can infer that e2=w+1 | e1<=e2 & u1<=u2 & i1<=i2 & s1<=s2 & t1<=t2, so some conditions omitted }
Ei1 Es1 Et1 Eu1 (((u1*w)+i1)*w+t1)*w+s1=e1 &                                    { (u,i,t,s) }
Ei2 Es2 Et2 Eu2 i2<w & s2<w & t2<w & (((u2*w)+i2)*w+t2)*w+s2=e2 &               { e2=1+w is initial state u=i=0, s=t=1 }
(e2=w+1 | e1=e2 | i2=i1+1+1 & s2=s1*(n+1) & t2=t1*n &                           { i=2n, s=(n+1)^n, mult=t=n^n, s/mult=e }
Eg1 Eg2 g1+1=(i2+i2)*(i2+i2) & g1*u1+mult=g1*u2+g2 & g2<g1) &                   { u/mult=sum[j=4,8,...,4n]1/(j*j-1)=(4-pi)/8. mult=g1*(u2-u1)+g2 }
(t>1 | i2=n+n & t2=mult & Ediff Ediff2                                          { check at an end t=1 }
c1*s2+c2*mult+c3*u2+diff=c4*s2+c5*mult+diff2 & k*(diff+diff2)<mult))            { |diff-diff2|<=diff+diff2<mult/k, so ...<1/k }

a|b&ces a|(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.

l4m2
fuente
¿Por qué puedes tomar mult = t? Además, dado xque solo puede tener un número finito de dígitos, deberá tener en cuenta lo e1 = e2 = 0suficientemente grande t. También necesitará más paréntesis u otra desambiguación para construcciones ambiguas como _ & _ | _.
Anders Kaseorg
@AndersKaseorg Multiplico cada artículo mult. No veo ningún problema mult=t2al final. e1=e2=0debería arreglarse pero no es tan cierto, por lo que actualmente no cambio la aceptación.
l4m2
Si a & b | ces (a & b) | casí, t*1=tdefinitivamente está en el lugar equivocado. Además, no ha excluido la solución trivial c1 = c4 & c2 = c5 & c3 = 0 & diff = diff2.
Anders Kaseorg
@AndersKaseorg ¿Por qué mi razón diff≠diff2funciona?
l4m2
De todos modos, puedo usar, !(c2=c5)como ya sabemos, ees irracional, por lo que incluso si esto no funciona, el puntaje no aumentará
l4m2 el