Calcul de la fonction de castor occupé

La fonction de décalage max du castor occupé, , a des valeurs connues pour . Y a-t-il une raison structurelle fondamentale pour laquelle il est inconcevable que nous trouvions un jour pour ? Qu'est-ce qui est si différent de que ? Ou ? Quelque part en cours de route, il doit y avoir une différence fondamentale, sinon serait, en principe, calculable pour tout , alors quelle est exactement cette différence? $S(n)$ $n\leq4$ $S(n)$ $n>4$ $n=4$ $n=5$ $n=6$ $S(n)$ $n$

computability busy-beaver PeteyPabPro
la source

Réponses:

La raison pour laquelle aucun programme ne peut calculer est que si vous saviez ce qu'est vous pourriez décider du problème d'arrêt - vous sauriez quand arrêter d'attendre. D'un autre côté, pour chaque il existe un programme qui calcule pour tout - il utilise simplement une table. $S(n)$ $S(n)$ $m$ $S(n)$ $n \leq m$

S'il était possible de prouver la valeur de pour tout (c'est-à-dire que pour tout nous pourrions prouver pour certains ), alors nous pourrions calculer en cherchant dans toutes les preuves ( cela suppose que notre système de preuve est valide). Donc, pour chaque système de preuve, il existe une valeur minimale de pour laquelle vous ne pouvez pas prouver que pour tout . $S(n)$ $n$ $n$ $S(n) = \alpha$ $\alpha$ $S(n)$ $n$ $S(n) = \alpha$ $\alpha$

Enfin, la raison pour laquelle nous connaissons est probablement parce que est un très petit nombre. Le chiffre est légèrement plus grand, et donc les choses se compliquent. Il n'y a pas de raison profonde pour laquelle nous connaissons mais pas , tout comme il n'y a pas de raison profonde pour laquelle nous connaissons le nombre de Ramsey mais pas (bien que les nombres de Ramsey soient bien sûr calculables) . $S(4)$ $4$ $5$ $S(4)$ $S(5)$ $R(4)$ $R(5)$

Yuval Filmus
la source

Merci. Le paragraphe du milieu était essentiellement ce que je me demandais (et c'est une preuve de Godel, n'est-ce pas?). Il se pourrait donc que

ait une preuve dans notre système formel, mais

non.

S (4)

$S(4)$

S (5)

$S(5)$

PeteyPabPro

Probablement. Si

n'est pas démontrable mais vrai que

est également non démontrable, et nous avons donc une déclaration qui ne peut être ni prouvée ni réfutée.

S (n) = " S (n) "

$S(n)=\text{"}S(n)\text{"}$

S (n) \neq " S (n) "

$S(n)\neq\text{"}S(n)\text{"}$

Yuval Filmus

Vous n'avez toujours pas vraiment expliqué pourquoi nous pouvons être si sûrs que S (4) est correct, tandis que S (5) ou plus nous ne le saurons jamais. Est-ce parce que nous ne sommes pas à 100% sur S (4), mais seulement "très presque" bien sûr?

Dan W

Nous sommes sûrs à 100% de S (4). Je ne pense pas qu'il y ait une raison profonde derrière notre ignorance concernant S (5). C'est juste la limite actuelle de nos connaissances.

Yuval Filmus

Je crois qu'il existe un système de preuve très solide et une machine de turing à 6 états et 2 couleurs de sorte qu'il peut être prouvé qu'il n'y a aucune preuve dans ce système qu'il ne s'arrêtera jamais et qu'il ne s'arrêtera avant aucun algorithme pouvant être prouvé dans ce système dans un googol caractères pour éventuellement arrêter les arrêts.

Timothy

$n$ $S(n)$

PeteyPabPro
la source

Pourriez-vous citer une partie pertinente?

Evil

un autre angle, avec une esquisse informelle d'une réponse, qui prendrait longtemps à s'étoffer techniquement avec d'autres recherches (c'est-à-dire qu'il s'agit essentiellement d'un programme de recherche): il existe des preuves préliminaires que la limite de ce qui est calculable à propos du Castor occupé La fonction est une mesure de la complexité de l'algorithme, avec deux références en dessous de cette indication dans cette direction. [1] [2] en gros, les petites MT avec très peu d'états ne peuvent pas accomplir "autant" ou "un comportement aussi sophistiqué" que des algorithmes plus complexes avec plus d'états. par conséquent, le calcul de celui-ci semble également avoir un lien profond avec la complexité de Kolmogorov . [3] une autre façon de voir les choses est que ce qui est connu / calculable sur la fonction Busy Beaver coïncide également étroitement avec l'état de l'art dans le théorème automatisé. prouver, qui (semblable au progrès technologique) est une frontière en constante évolution basée sur la recherche en mathématiques et en informatique.

[1] Problème de castor occupé, une nouvelle attaque du millénaire , van Heuveln et al

[2] Petites machines de Turing et compétition généralisée de castors occupés , Michel

[3] Sur le temps d'exécution des problèmes les plus courts , Batfai

vzn
la source