Un langage de programmation qui ne peut implémenter que des fonctions bijectives calculables?

Existe-t-il des langages de programmation (ou logique) qui peuvent implémenter (ou exprimer) une fonction si et seulement si est une fonction bijective calculable? $f:\mathbb{N}\to \mathbb{N}$ $f$

reference-request programming-languages logic reversible-computing Chao Xu
la source

Quelqu'un m'a prouvé qu'il est impossible de créer un langage qui n'accepte que les programmes de terminaison. Puisque votre question est assez similaire, je suppose que non.

FUZxxl

Il semble peu probable qu'il y ait un tel langage de programmation, je suppose que vous pourriez essayer de l'imposer, mais vous ne seriez pas en mesure de faire des choses simples comme le tri, du moins pas sans qu'il devienne horriblement complexe et douloureux.

Luke Mathieson

@FUZxxl Cela ne capture pas beaucoup de programmes de terminaison, en fait même la fonction f (x) = 1 est impossible à exprimer dans ce langage. J'ai également le sentiment que ce type de fonctions est capturé par la programmation fonctionnelle totale puisque chaque fonction est une fonction totale.

Chao Xu

@FUZxxl, je ne pense pas que ce soit vrai, mais un tel langage devrait être limité. Par exemple, un langage équivalent aux automates déterministes finis serait garanti de se terminer, mais serait extrêmement limité dans ce qu'il pourrait calculer.

jmite

@FUZxxl, les détails d'une telle déclaration sont importants. Il est facile de concevoir un langage de programmation dans lequel chaque programme se termine. C'est une autre chose que de concevoir un langage dans lequel nous pouvons exprimer chaque fonction calculable.

Vijay D

Réponses:

Il n'y a pas un tel langage.

Cependant, jetez un œil à Boomerang . C'est un langage pour écrire des bijections entre les chaînes. Je ne sais pas dans quelle mesure une classe de cartes y est exprimable, mais je suis sûr que vous pouvez savoir si vous recherchez un peu.

Il est raisonnable d'exiger d'un langage de programmation que l'ensemble des programmes valides soit reconnaissable par un interprète ou un compilateur, c'est-à-dire qu'il s'agisse d'un ensemble énumérable par ordinateur. Supposons alors que nous disposions d'un langage de programmation dont l'ensemble des programmes valides était calculable et qui implémentait précisément toutes les bijections calculables . Cela impliquerait que nous pouvons énumérer de manière calculable toutes les bijections calculables (simplement énumérer tous les programmes valides dans ce langage de programmation), mais cela est impossible par le théorème suivant. $\mathbb{N} \to \mathbb{N}$

Théorème: Supposons que est une séquence calculable de bijections calculables. Ensuite, il y a une bijection calculable qui n'est pas dans la séquence. $f_0, f_1, f_2, \ldots$

Preuve. Nous construisons une bijection comme suit. Pour définir les valeurs et , nous regardons : $g : \mathbb{N} \to \mathbb{N}$ $g(2 k)$ $g(2 k + 1)$ $f_k(2 k)$

si alors réglez et , $f_k(2 k) = 2 k$ $g(2 k) = 2 k + 1$ $g(2 k + 1) = 2 k$
si alors et . $f_k(2 k) \neq 2 k$ $g(2 k) = 2 k$ $g(2 k + 1) = 2 k + 1$

Clairement, pour chaque , est différent de car . De plus, est calculable et c'est une bijection car c'est son propre inverse. QED. $k \in \mathbb{N}$ $g$ $f_k$ $g(2 k) \neq f_k(2 k)$ $g$

Andrej Bauer
la source

Pourquoi avez-vous même besoin de cette astuce et ? Utiliser devrait suffire.

2 k

$2k$

2 k + 1

$2k+1$

g (k) = f_{k} (k) + 1

$g(k)=f_k(k)+1$

FUZxxl

@FUZxxl: si vous utilisez la fonction résultante n'est pas surjective

f_{k} (k) + 1

$f_k(k)+1$

Vor

Vous devez vous assurer que est bijectif.

g

$g$

Andrej Bauer

La déclaration initiale est fausse, il existe de nombreuses langues de ce type dans la littérature.

Nathaniel

En revanche votre preuve semble légitime. Peut-être que je suis confus en quelque sorte. Je dois lire attentivement le document d'Axelsen et de Glück (voir ma réponse) pour comprendre ce qui se passe ici.

Nathaniel