Agrégation informatique externe 2024, épreuve 3Sujet et rapport du jury

AGREGATION
CONCOURS EXTERNE

• -ÉTUDE DE CAS INFORMATIQUE
• -FONDEMENTS DE L'INFORMATIQUE

INFORMATION AUX CANDIDATS

• -Etude de cas informatique :
  

  

• -Fondement de l'informatique :
  

  

Épreuve spécifique

Étude de cas informatique

Description du système étudié

Partie I. Application mobile

Figure 1 - IHM de la page de suivi d'un match accessible pour un spectateur. Le contenu de la page est centré et les polices sont volontairement agrandies pour faciliter la lecture des informations importantes. De haut en bas, les liens hypertextes permettent d'accéder à la liste des matchs en cours et le(s) classement(s) de la compétition. Le temps restant indique le nombre de minutes et secondes à jouer avant la fin du temps officiel. En cas d'application du "cap à 1", le temps restant compte à partir de zéro jusqu'à ce que le vainqueur du match soit désigné. L'historique des scores, indiqué dans la partie inférieure de l'écran, liste la séquence des précédents scores du match.

Partie II. Gestion d'un match d'ultimate

class Equipe:
    def __init__(self,name):
        self._name = name
    def __str__(self):
        return self._name
    def __repr__(self):
        return f'Equipe({self._name})'

class Match:
    def __init__(self, locaux, visiteurs):
        if locaux == visiteurs:
            raise Exception("Les équipes doivent être distinctes.")
        self._score = {locaux:0, visiteurs:0}
        self._dernier = None
    def equipes(self):
        return self._score.keys()
    def score(self):
        return self._score.copy()
    def gagnant(self):
        return max(self._score, key=self._score.get)
    def perdant(self):
        return min(self._score, key=self._score.get)
    def marquerPoint(self, equipe):
        self._score[equipe] += 1
        self._dernier = equipe
    def annulerPoint(self):
        if self._dernier is None:
            raise Exception("Aucun point à annuler.")
        self._score[self._dernier] -= 1
        self._dernier = None
    def __str__(self):
        return self._score

CREATE TABLE Equipes (
    EquipeID INT PRIMARY KEY AUTO_INCREMENT,
    Nom VARCHAR(255) NOT NULL UNIQUE
);
CREATE TABLE Matchs (
    MatchID INT PRIMARY KEY AUTO_INCREMENT,
    EquipeAID INT,
    EquipeBID INT,
    FOREIGN KEY (EquipeAID) REFERENCES Equipes(EquipeID)
    FOREIGN KEY (EquipeBID) REFERENCES Equipes(EquipeID)
);
CREATE TABLE HistoriqueScores (
    HistoriqueID INT PRIMARY KEY AUTO_INCREMENT,
    MatchID INT,
    ScoreEquipeA INT,
    ScoreEquipeB INT,
    Estampille TIMESTAMP DEFAULT CURRENT_TIMESTAMP,
    FOREIGN KEY (MatchID) REFERENCES Matchs(MatchID)
);

Partie III. Gestion de tournois d'ultimate

Partie IV. Gestion d'une compétition en divisions

Partie V. Gestion d'un tournoi hat

class Vehicule:
    def __init__(self,conducteur,capacite,depart,distances):
        self._conducteur = conducteur
        self._capacite = capacite
        self._position = depart
        self._distances = distances
        self._distance = 0
        self.passagers = []
    def places_disponibles(self):
        return self._capacite - len(self.passagers)
    def distance_parcourue(self):
        return self._distance
    def ajouter_passager(self,passager):
        if self.places_disponibles() == 0:
            raise ValueError("Le véhicule est complet")
        self.passagers.append(passager)
    def visiter_ville(self,ville):
        if ville in self._distances:
            self._distance += self._distances[self._position][ville]
            self._position = ville

Fondements de l'informatique

Partie I. Théorème de complétude

I. 1 Restriction de l'ensemble des formules

• 2.a) ¬(A ∨ B) ≡ ¬A ∧ ¬B;
• 2.b) ¬(A ∧ B) ≡ ¬A ∨ ¬B.

I. 2 Démonstration du théorème de complétude

• -si [ [A] ]_v = V, alors le séquent h_v⊢A est dérivable;
• -si [ [A] ]_v = F, alors le séquent h_v⊢¬A est dérivable.

Partie II. Mécanisation de la recherche de preuve

• -certaines règles, comme ∨ _e et → _e, nécessitent de trouver une formule qui n'apparaît pas nécessairement dans le contexte initial. Trouver une telle formule de manière automatique ne paraît pas aisé.
• -il est possible de « se tromper » en construisant un arbre de preuve, par exemple si l'on applique la règle ∨ _(i, g) alors que c'était le membre droit de la disjonction qui était démontrable.

• -un séquent Γ⊢A est dérivable en déduction naturelle si et seulement s'il l'est également en calcul des séquents;
• -un séquent Γ⊢Δ est dérivable en calcul des séquents si et seulement si le séquent Γ⊢⋁_(A ∈ Δ)A l'est également en déduction naturelle.

• 16.a) ⊢¬¬A ↔ A
• 16.b) ⊢¬(A ∨ B) ↔ (¬A ∧ ¬B).

type 'a formule =
    | Faux
    | Var of 'a
    | Non of 'a formule
    | Et of 'a formule * 'a formule

type 'a sequent =
    {hyp : 'a formule list; concl : 'a formule list}

• -une fonction extrait : 'a -> 'a list -> 'a list telle que extrait x l supprime la première occurrence de x dans l s'il en existe une et lève l'exception Not_found sinon;
• -une fonction element_commun : 'a list -> 'a list -> 'a option qui renvoie un élément commun aux deux listes passées en argument, sous la forme Some x, s'il en existe un, et None sinon.

type 'a derivation =
    | Axiome of 'a formule
    | Faux_g
    | Non_g of 'a formule * 'a derivation
    | Non_d of 'a formule * 'a derivation
    | Et_g of 'a formule * 'a derivation
    | Et_d of 'a formule * 'a derivation * 'a derivation

Et_d (Et (Var "p", Var "q"),
    Axiome (Var "p"),
    Non_d (Non (Var "q"), Axiome (Var "q")))

• 1.S'il existe dans Γ une formule A non atomique, appliquer la règle correspondant au connecteur logique principal de A, puis construire récursivement une dérivation des prémisses de cette règle.
• 2.Sinon, s'il existe dans Δ une formule non atomique, procéder de même en appliquant la règle correspondante et en démontrant récursivement les prémisses de cette règle.
• 3.Sinon, appliquer l'une des deux règles ⊥ _g et ax si possible et échouer sinon.

Partie III. Passage à la logique du premier ordre

Figure 4 - Termes et formules de la logique du premier ordre

III. 1 Calcul des séquents pour la logique du premier ordre

III. 2 Unification

Question 26.

• 26.a) Montrer que les termes t = f(x, y) et u = f(f(y, z), a ), où a ∈ S_F est une constante et f ∈ S_F est d'arité 2 , sont unifiables.
• 26.b) Que peut-on dire de la réponse au problème Unif si l'on considère l'instance
  L = [f(x, y) = ^?f(f(y, z), a), f(z, y) = ^?f(f(y, z), a)]?

• - L_0 = L et σ_0 est la fonction identité;
• - L_(n + 1) et σ_(n + 1) sont calculés comme suit :
  • -Si L_n = [] : l'algorithme se termine et σ_n est un unificateur pour L.
  • -Si L_n = (f(t_1, …, t_p) = ^?g(u_1, …, u_q)) : L^′ avec f, g ∈ S_F et t_1, …, t_p, u_1, …, u_q ∈ T :
    • -si f ≠ g, alors l'algorithme échoue : il n'y a pas d'unificateur pour L;
    • -si f = g (et donc p = q ), alors L_(n + 1) = [t_1 = ^?u_1, …, t_p = ^?u_p]@L^′ et σ_(n + 1) = σ_n.
  • -Si L_n = (x = ^?x) : L^′ avec x ∈ V : L_(n + 1) = L^′ et σ_(n + 1) = σ_n;
  • -Si L_n = (x = ^?t) : L^′ avec x ∈ V et t ∈ T∖{x}, à symétrie de l'équation près :
    • -si x ∈ FV(t), alors l'algorithme échoue : il n'y a pas d'unificateur pour L;
    • -sinon, σ_(n + 1) = (x:=t) ∘ σ_n et L_(n + 1) = L^′[x:=t], où [t_i = ^?u_i, i ∈ [ [1, n] ]][x:=t] = [t_i[x:=t] = ^?u_i[x:=t], i ∈ [ [1, n] ]].

type ('a, 'b) terme =
    | Var of 'a
    | App of 'b * ('a, 'b) terme list

type ('a, 'b) subst = ('a * ('a, 'b) terme) list
type ('a, 'b) instance = (('a, 'b) terme * ('a, 'b) terme) list

• 28.a) est_variable : 'a -> ('a, 'b) terme -> bool telle que est_variable x t calcule le booléen x ∈ FV(t);
• 28.b) substitue : 'a -> ('a, 'b) terme -> ('a, 'b) terme -> ('a, 'b) terme telle que substitue x u t calcule le terme t[x:=u].

• - t_0 = u_0 = x_0;
• -pour tout n ∈ ℕ, t_(n + 1) = f(t_n, x_n) et u_(n + 1) = f(x_n, u_n).