Je n'ai remarqué qu'après avoir enregistré la vidéo que mon visage s'est sali à cause du marqueur ! Ça a l'air si drôle, désolé pour ça. Les bases de calcul lambda sont dans • Programmation Fonction...
Timecodes 00:00:40 Partie I. Codage d’entiers de Church 00:01:27 Booléens et conditionnelles 00:08:00 Nombres entiers dans le codage de Church 00:10:00 Operations arithmetiques: succ, plus, mult, exp 00:14:40 Exercice: 1 + 2 = 3 00:19:20 Exercice: 2^2 = 4 00:26:00 Plus [i] [j] = [i+j], Preuve par recurrence 00:27:30 Cas de base, [i] = [0] 00:32:30 Hypothèse de recurrence, passage de [i] vers [i+1] 00:41:40 Partie II. Equations recursives 00:42:20 Exercice. GX = XXX, G = ? 00:43:52 Exercice. F x = x I, F = ? 00:45:18 Annonce: F x = F, F = ? plus difficile que les précédents. 00:46:05 Construction de predicat EstZero (Church) 00:56:00 La formulation de théorème de point fixe FX = X, X=? 00:57:08 Combinateur de point fixe Y tel que Y n = n (Y n) 01:01:40 Démonstration de théorème 01:05:07 Exercice. Fx = F, F=? 01:09:35 Exercice. Fx = xF, F=? 01:11:35 Recursion avec le combinateur de point fixe, principe général 01:12:12 Exemple: addition de deux entiers avec la recursion 01:18:30 Exercice (sans corrigé), factorielle de n? 01:18:50 Partie III. Arithmétique de Barendregt 01:19:55 Construction de paire 01:21:00 Exercice: fst, snd? 01:22:40 Codage d’entiers de Barendregt 01:23:22 predicat EstZero dans le codage de Barendregt 01:24:30 Exercice (sans corrigé): Autres operations arithmétiques dans ce codage. 01:25:35 Exercice: Théorème de points fixes multiples 01:29:15 Divertissement (thisisafixedpointcombinator)
Bonjour En premier lieu je tiens à souligner la qualité de ta vidéo Je suis actuellement en MPSI et je m'intéresse au lambda calcule pour mes cours d'info est-ce que tu pourrais expliquer comment calculer le prédécesseur d'un entier n de Church Je n'ai pas encore fini la vidéo mais il me semble que tu n'en parle pas Je suis en train d'essayer de faire cette fonction sur caml et je suis un peu perdu
à et je vois que tu as fait des video sur la théorie musicale mais je ne parle pas ta langue si jamais tu en refais en français ou en anglais je suis preneur
@@verbalkint8363 avec recursion / theoreme de point fixe c'est tout à fait possible. Par exemple, voir le morceau autour 1:12:38. Le video sur la theorie musicale etait quand j'etais à l'universite à Moscou, peut être un jour je vais le refaire en Anglais
Il y en a effectivement deux codages d'entiers (Church et Barendregt), ils sont plus ou moins interexchangeable à l'aide des théorèmes de recursion. C'est bizzare que je n'ai pas raconté le Pred car c'est basique. Alors pour Barendregt le predecesseur corresponds aux operations arborescentes (gauche / droite), mais pour le codage du Church c'est different
