Sofus aux RMLL de 2016
Cette partie de l’article avait été rédigée pour le (défunt) site spip des RMLL de Saint-Joseph en juillet 2016. Un atelier Sofus avait été animé sur un stand lors de ces RMLL.
Sofus est un langage de programmation spécialisé dans la description des programmes de calcul comme on en voit fréquemment au brevet des collèges. Par exemple voici un extrait du sujet du brevet des collèges 2016 :
On considère les deux programmes de calcul ci-dessous :
Programme A
- Choisir un nombre.
- Multiplier par -2.
- Ajouter 13.
Programme B
- Choisir un nombre.
- Soustraire 7.
- Multiplier par 3.
Voici comment les deux programmes peuvent être programmés dans Sofus :
On le voit, Sofus intègre la technologie Blockly qui permet de programmer en Sofus sur une tablette tactile voire un smartphone. Sofus présente les particularités suivantes :
- possibilité d’exporter les programmes de calcul au format Xcas pour prouver des propriétés à l’aide du calcul formel ;
- calcul exact sur les fractions ;
- Programmation de robots (pour l’instant virtuels) de type « tortue logo (langage) » pour le graphisme et export des figures obtenues au format svg.
Bien que rapide, la tortue de Sofus peut dessiner un escargot :
Voici le programme Sofus ayant donné ce dessin :
Pour en savoir plus :
- Un interpréteur en ligne (sans les tortues pour l’instant) ;
- Un article sur la programmation au collège, parlant entre autres, de Sofus ;
- Un article sur le graphisme tortue, d’où est extraite cette figure dessinée avec Sofus :
Après les RMLL
Suite à cette présentation et aux retours des collègues présents, a été proposé ce corrigé du sujet zéro du DNB :
Et ces exemples de sujets de type DNB (les images sont cliquables et mènent à des fiches d’exercices) :
Vers la fin des années 1930, Alonzo Church a émis l’hypothèse que toute définition raisonnable de ce qu’est une fonction calculable, coïncide avec les définitions connues alors (fonctions primitives récursives, lambda-calcul, machines de Turing), sous la forme de la thèse de Church : pour toute fonction calculable, il existe une machine de Turing permettant de calculer les valeurs de cette fonction.
On appelle donc Turing-complet un langage de programmation permettant de calculer ce que les autres langages de programmation permettent de calculer. Un exemple connu aujourd’hui est Python.
Pour prouver la Turing-complétude de Python, on programme en Python un interpréteur ou un compilateur d’un autre langage de programmation que l’on sait Turing-complet (le plus souvent c’est Brainf*ck). Pour prouver la Turing-complétude de Sofus on va lui préférer un interpréteur du langage de programmation Fractran. Le voici (un clic sur l’image permet de télécharger le fichier Sofus à tester en ligne sur le site sofus) :
Théorème (Conway) : Fractran est Turing-complet.
L’interpréteur ci-dessus permet alors d’en déduire le
Corollaire (Busser) : Sofus est Turing-complet.
Commentaires