Запишите это в стиле теории чисел

19

Напишите математическое утверждение, используя символы:

  • There exists at least one non-negative integer(записывается как Eэкзистенциальный квантификатор)
  • All non-negative integers(записывается как Aуниверсальный квантификатор)
  • + (Дополнение)
  • * (Умножение)
  • = (Равенство)
  • >, <(операторы сравнения)
  • &(и), |(или), !(не)
  • (, )(для группировки)
  • имена переменных

что эквивалентно утверждению

Существует рациональное число a, такое, что π + e * a рационально.

(конечно, является математической константой, равной окружности, деленной на диаметр круга, а является числом Эйлера )πзнак равно3,1415 ...езнак равно2,7182 ...

Вы должны доказать, что ваше утверждение действительно эквивалентно приведенному выше.

Очевидно, что «самый короткий» способ сделать это - доказать утверждение, истинное или ложное, и затем ответить тривиально истинным или ложным утверждением, поскольку все истинные утверждения эквивалентны друг другу, как и все ложные утверждения.

Однако значение истинности данного утверждения является нерешенной проблемой в математике : мы даже не знаем, является ли иррациональным! Поэтому, за исключением инновационных математических исследований, задача состоит в том, чтобы найти «простое» эквивалентное утверждение, доказать его эквивалентность и описать его как можно более кратко.π+е

счет

E A + * = > < & |и !каждый добавляет 1 к баллу. (и )ничего не добавляйте к счету. Каждое имя переменной добавляет 1 к баллу.

Например, E x (A ba x+ba>x*(x+ba))оценка 13 ( E x A ba x + ba > x * x + ba)

Самый низкий балл побеждает.


Замечания:

Отказ от ответственности: это примечание не было написано ФП.

  • Это не вызов. Ответы не обязательно должны содержать код.
  • Это похоже, но не на , так как вам нужно написать утверждение и доказать, что оно эквивалентно другому утверждению.
  • Вам разрешено представить тривиально-истинное (например, для всех x, x = x Ax x=x) или тривиально-ложное утверждение (например, для всех x, x> x Ax x>x), если вы можете доказать, что приведенное выше утверждение является истинным / ложным.
  • Вам разрешено использовать дополнительные символы (аналогично лемме в пробном гольфе), но счет будет засчитан так же, как вы их не используете.
    Например, если вы укажете a => bзначение (!a) | b, каждый раз, когда вы используете =>доказательство, ваш счет увеличивается на 2.
  • Поскольку константы не указаны в разрешенных символах, вы не должны их использовать.
    Например: утверждение 1 > 0может быть записано как

    
    Forall zero: ( zero + zero = zero ) =>
    Forall one: ( Forall x: x * one = x ) =>
    one > zero
    

    на счет 23. (помните, что =>стоит 2 за использование).

Советы

  • Вы можете использовать натуральные константы E0, 0+0=0 & E1, At 1*t=t &(так что вам не нужно, =>что более обширно); для чисел больше 1, просто добавьте 1
l4m2
источник
5
Мне нравится концепция здесь, но утверждение действительно сложно написать, и я буду впечатлен любым решением, независимо от оценки. Я бы предложил использовать что-то более простое, чтобы больше людей участвовало.
xnor
1
Вам требуется математическое утверждение, которое эквивалентно данному. В каком смысле они должны быть эквивалентны ? Если я прав, данное утверждение является ложным. Так что его эквивалентность с другими утверждениями мне трудно понять. Например, эквивалентно ли существует рациональное число a, такое, что i + e * a рационально (где i - мнимая единица)?
Луис Мендо
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.. В заявлении не теперь ни доказано , ни опровергнуто, так что я действительно не возражаю , если проблема становится скучно , потому что такая проблема решается
l4m2
1
Вопрос в том виде, в котором он был написан, казалось, по большей части похоронил лиду и не объяснил, что на самом деле происходит, поэтому я написал небольшое пояснение в примечаниях (что нетривиальность задачи зависит от неизвестной в настоящее время истинности данного утверждения) ,
Линн
I'd be impressed by any solution no matter the score.Счет был только для того, чтобы нацелиться на тех, кто может решить эту проблему
l4m2

Ответы:

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))))))))))))))))))))))))))

Как это устроено

Во-первых, умножьте на предполагаемые общие знаменатели a и (π + e · a), чтобы переписать условие следующим образом: существуют a, b, c ∈ ℕ (не все нули) с a · π + b · e = c или a · π - b · e = c или −a · π + b · e = c. Три случая необходимы для решения проблем со знаком.

Затем нам нужно переписать это, чтобы говорить о π и e через рациональные приближения: для всех рациональных приближений π₀ <π <π₁ и e₀ <e <e₁, мы имеем · π₀ + b · e₀ <c <a · π₁ + b · e₁ или a · π₀ - b · e₁ <c <a · π₁ + b · e₀ или −a · π₁ + b · e₀ <c <−a · π₀ + b · e₁. (Обратите внимание, что теперь мы получаем условие «не все ноль» бесплатно.)

Теперь о трудной части. Как мы получаем эти рациональные приближения? Мы хотим использовать формулы как

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 ,

но нет очевидного способа написать итерационные определения этих продуктов. Итак, мы создаем немного механизма, который я впервые описал в этом посте Quora . Определение:

делит (d, a): = ∃b, a = d · b,

powerOfPrime (a, p): = ∀b, ((b> 1 и делит (b, a)) ⇒ делит (p, b)),

который выполняется тогда и только тогда, когда a = 1, или p = 1, или p простое и a является степенью его. потом

isDigit (a, s, p): = a <p и ∃b, (powerOfPrime (b, p) и ∃qr, (r <b и s = (p · q + a) · b + r))

выполняется тогда и только тогда, когда a = 0, или a является цифрой от числа base-p s. Это позволяет нам представлять любой конечный набор, используя цифры некоторого числа base-p. Теперь мы можем перевести итеративные вычисления, написав, примерно, что существует набор промежуточных состояний, таких, что конечное состояние находится в наборе, и каждое состояние в наборе является либо начальным состоянием, либо в одном шаге следует из некоторого другого состояния в устанавливать.

Подробности в коде ниже.

Генерация кода в 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 "")

Попробуйте онлайн!

Андерс Касеорг
источник
«который удовлетворяется тогда, когда a = 1, или p простое, а a является степенью его» - вы также можете иметь p = 1. Хотя p> 1 подразумевается isDigit, единственное место, где вы его используете.
Орджан Йохансен
@ ØrjanJohansen Спасибо, я исправил эту заметку. (На самом деле не имеет значения, какие наборы powerOfPrimeи в isDigitконечном итоге представляют в неожиданных случаях, если есть какой-то способ представить каждый конечный набор.)
Anders Kaseorg
2
aДумаю, если у него 7 или выше, то стоит добавить ex (\a' -> a' := a :& ... )обертку isDigit.
Орджан Йохансен
@ ØrjanJohansen Конечно, это экономит 68. Спасибо!
Андерс Касеорг
Я считаю, что вам нужно требовать k>0, так как eBoundдает нулевой знаменатель (и один нулевой числитель) в этом k==0случае, поэтому все альтернативы терпят неудачу.
Орджан Йохансен
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&cЭто a|(b&c)потому, что я думаю, что удаление этих скобок делает его лучше, в любом случае, они бесплатны.

Использовал JavaScript "(expr)".replace(/\{.*?\}/g,'').match(/[a-z0-9]+|[^a-z0-9\s\(\)]/g)для подсчета токенов.

l4m2
источник
Почему ты можешь взять mult = t? Кроме того, так как xможет иметь только конечное число цифр, вам нужно учитывать e1 = e2 = 0достаточно большой t. Также вам понадобится больше скобок или другой неоднозначности для неоднозначных конструкций, таких как _ & _ | _.
Андерс Касеорг
@AndersKaseorg Я умножаю каждый элемент mult. Не вижу проблем mult=t2в конце. e1=e2=0должно быть исправлено, но не так точно, поэтому в настоящее время я не изменяю принятие.
м2 19
Если a & b | cэто (a & b) | cто, что вы t*1=t, безусловно, не в том месте. Также вы не исключили тривиальное решение c1 = c4 & c2 = c5 & c3 = 0 & diff = diff2.
Андерс Касеорг
@AndersKaseorg Есть ли у меня причина, почему diff≠diff2работать?
м2 19
В любом случае я могу использовать, !(c2=c5)как мы уже знаем e, иррационально, поэтому, даже если это не сработает, счет не увеличится
l4m2