tiens http://www.yveslemaire.fr/info/poly.pdf c'est le poly du cours d'info que j'ai suivi en prépa. Il y a un rappel de caml et puis pas mal de trucs sur les structures de données et les langages. Ça devrait couvrir 75% du programme.
(Je suis retombé dessus par hasard, sinon je te l'aurais passé avant).
Je transfers ici un post d'un fil où il était mal placé
Oui, je me rappelle: j'allais suivre un cours de Rached sur les formes quadratiques et d'ailleurs c'était très bien ce cours
Merci, et promis.... je vous dirai même mes notes (entre 0,1 et 1,5) et demanderai une photocopie de mes copies pour les poster... je trouve ça rigolo
En fait, j'ai renoncé à m'en occuper (mes excuses aux quelques personnes qui ont pu vouloir m'aider, mais je suis irrécupérable au moins à court terme, et je bosse sur ma psychanalyse.. donc espoir à long terme peut-être),
même si 1mois peut paraitre long, je ne pouvais pas (pour raisons diverses, et persos) tenter une sorte de big focalisation au mois de juin pour tenter le diable et je ne me porte que mieux de ne plus y penser, d'avoir revu mon lycée, etc, bref le quotidien des gens normaux.
Je pense surtout à profiter de "mon addiction" à ce forum pour prendre le tps de réfléchir au programme de maths de l'agreg tout au long de l'an prochain "tranquillement"*** (en espérant ne pas retomber dans de la vélléité maladive) car ça n'a aucun sens de "bourrer" comme ça dans un court délai, non seulement on n'apprend finalement rien mais compte-tenu de ma perception assez perso des maths, j'ai l'impression que les gens dans mon cas désapprennent en se forçant comme des bourrins** (j'ai bien passé quelques soirées début juin dans des bars avec les livres que j'avais achetés, mais le stress me les faisait parcourir trop vite et leur taille m'empéchait de les lire tranquillement (c'est une question d'équilibre).
***Mais faudra que je me force à trainer un peu ds les fils que j'évite systématiquement, genre alg linéaire d'école, analyse d'école, exemples, etc
L'avantage de cette évènement incongru est que j'ai découvert**** camL (voir ci-dessous) et ça m'a donné aussi des "idées" (j'ai découvert qu'existe une forme d'analyse qui a une essence un peu arithmétique (voir fil sur e et pi/2 récent) au détour d'une séance zen où je voulais tenter de me réintéresser à "un programme scolaire" en essayant d'y instiller mes fantasmes (mondes parallèles, voyance, temps, logique)
[size=x-small]**Au bout de quelques heures, je ne voyais plus ce que je lisais et même les écriteaux dans la rue, je ne les comprenais plus, et j'ai ressenti plein de douleurs physiques (psychosomatiques probablement bref... snif, être barjeau a des inconvénients..)[/size]
**** j'y ai passé du tps sur ce langage fascinant, hélas, sans vraie doc, et hélas dans mon environnement PC (j'ai le flemme d'aller sur le CD que j'ai installé... qu'est-ce que je suis con..) avec une fenetre ms dos et de la grosse galère pour exécuter et débugguer
Voici mon programme dont je suis le plus fier:
Tenez-vous bien: il prend un lambda terme, l'exécute intégralement en un terme normal et le tout sans aucun effort, ni "renommage" des variables liées (ce renommage est toujours un truc d'une chiantise absolue, et je voulais le contourner d'une manière élégante... mission accomplie lol, pas un minipet de renommage, 100% bio, 100% métaphysique)
Vous constaterez que le type "tera" ne prévoit même pas la possibilité d'un redex, c'est ça qui me fait le plus kiffer. Quant à l'application "ap", admirez sa concision... Arrrg, c'est dommage que je n'ai pas d'environnement caml convivial pour windows (à la delphi), car je m'éclaterais..
Voici le code:
remplacé, voir code suivant
Je n'ai pas fait d'entrées sorties, mais ça ne saurait tarder
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
J'ai modifié le code pour le rendre (légèrement) plus convivial:
type fo = V of string | I of fo*fo
type term = H of fo | A of fo*term*term | Lam of fo*fo*term
type tera = N of ts | L of fo*(tera->tera) and ts = Af of fo | Op of fo*ts*tera
let programmm = begin
let formule t=match t with
|H(x)->x
|A(y,u,v)->y
|Lam(x,y,w)->x
in
let rec test t =match t with
|H(x)->true
|A(x,u,v)->if (formule u) = I((formule v),x) then true else false
|Lam(x,y,w)->if x=I(y,(formule w)) then true else false
in
let formul1 t=match t with
|Af(p)->p
|Op(x,u,v)->x
in
let formul2 t=match t with
|N(x)->formul1 x
|L(p,f)->p
in
let conc p=
match p with |I(h,c)->c
in
let ap u v =match u with
|L(p,f)->f v
|N(x)->N(Op(conc (formul1 x),x,v))
in
let rec auxi t u p = match t with
|N(Af(x))->if x=p then u else t
|L(e,f)->let g x= (auxi (f x) u p) in L(e,g)
|N(Op(q,s,w))->let a=auxi (N s) u p in ap a (auxi w u p)
in
let rec traduction t = match t with
|H(p)->N(Af p)
|A(f,u,v)->ap (traduction u) (traduction v)
|Lam(a,x,w)->let ww=traduction w in let gg z = auxi ww z x in L(a,gg)
in
let rec detrad t = match t with
|L(p,f)-> (match p with |I(h,c)->Lam(p,h, (detrad (f (N(Af(h)) ) ) ) ) )
|N(x)->(match x with |Af(p)->H(p) |Op(q,u,v)->A(q,detrad (N(u)),detrad v) )
in
let normalize t = detrad (traduction t)
in
let rec ecri f = match f with
|V(x)->x
|I(x,y)->"("^(ecri x)^")->("^(ecri y)^")"
in
let rec lire s=
begin
print_string(s^"\n");
let a= read_line() in
if a="-" then I((lire "hypothèse?"),(lire "conclusion?")) else V(a)
end
in
let rec estdan p m=match m with
|[]->false
|x::n->if x=p then true else estdan p n
in
let rec prouve f m=
begin
if estdan f m then print_string ("tu prouves "^ (ecri f)^",\n mais tu pourrais t'en dispenser car tu l'as deja suppose\n") else
print_string ("tu prouves "^(ecri f)^"\n");
match f with
|V(x)->begin print_string "axiome (&) ou raison ..?\n";let a=read_line() in if a="&" then H(f) else
let r=lire "ta raison?" in A(f,(prouve (I(r,f)) m), (prouve r m) ) end
|I(h,c)->begin print_string "axiome (&) ou raison.. ou prendre hypothèse (!)\n";
let a=read_line() in if a="&" then H(f) else if a="!" then Lam(f,h,(prouve c (h::m))) else
let r=lire "ta raison?" in A(f,(prouve (I(r,f)) m ), prouve r m) end end
in
let rec epanoui t = match t with
|H(x)->"["^ecri x^"]" |A(f,u,v)->"("^(epanoui u)^").("^(epanoui v)^")["
^(ecri f)^"]" |Lam(f,h,w)->"admettant "^(ecri h)^(epanoui w)^"["^(ecri f)^"]"
in let f=lire "tu veux prouver quoi?" in
let t=prouve f [] in
print_string("ficher pour enregistrer la preuve?\n");
let mf=read_line() in
let fich=open_out mf in
output_string fich (epanoui t);
close_out fich
end
A l'exécution, le programme vous demande ce que vous voulez prouver
Pour entrer un phrase atomique vous rentrer un suite de caractère (évitez parenthèse et crochets)
Pour entrer une implication, vous tapez "-"
ensuite il vous demdande récursivement votre conclusion, puis votre hypothèse
Une fois rentrée votre affirmation, il vous demande de la prouver "à l'envers" (ie vous remontez vers les axiomes de votre choix)
Si à un moment vous voulez prouver A--->B en "supposant A", vous tapez "!"
Si à un moment vous ne souhaitez pas justifier, vous tapez "&"
Si vous souhaitez évoquer une raison (modus ponens), vous tapez D'ABORD n'importe quoi sauf "&","!" (le mieux c'est de taper directement sur "entrée" et là vous entrez votre raison (sur le même mode que vous avez entré votre phrase affirmée de départ
Puis il vous demandera récursivment de prouver raison puis raison ---->votre dernier truc
A la fin, il vous demande dans quel fichier vous souhaitez enregistrer votre preuve et l'y écrit, mais en la normalisant d'abord.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Bon en fait, à y bien regarder tu fais du shallow embedding mais sans vouloir le dire. C'est à dire que tu te reposes sur CAML pour faire la normalisation pour toi. Notamment cela te permet de te servir aussi de caml pour la notion de lieur en codant un lambda comme une fonction. Par contre, si tu veux afficher tes termes tu es obligé de réintroduire un nom de variable. Voila un exemple de code simplifié :
type term = FreeVar of string | App of term * term | Lam of (term -> term)
let rec normalise = function
| FreeVar x -> FreeVar x
| App(Lam f, t) -> normalise (f(t))
| App(u, v) -> normalise (App(normalise u, normalise v))
| Lam f -> Lam (fun t -> normalise (f(t)))
let rec string_of_term = function
| FreeVar x -> x
| App(u,v) -> "("^(string_of_term u)^")"^(string_of_term v)
| Lam f -> "\\x."^(string_of_term (f(FreeVar "x")))
let test = App(Lam(fun x -> x), FreeVar "y")
let _ =
print_string (string_of_term test);
print_newline();
print_string (string_of_term (normalise test));
print_newline()
Merci DFF, et bien j'avoue que l'illusion métaphysique que donne camL est vraiment agréable.
Voici un exemple qui ne sert à rien (il fait boucler la machine), mais qui devrait inciter les passionnés de philosophie du forum à ultiliser ce langage:
# type magique = L of (magique->int);; type magique = L of (magique -> int)
# let pick x=match x with |L(f)->f x;; val pick : magique -> int = <fun>
# let diag = L(pick);; val diag : magique = L <fun>
# let entierdivin=pick diag;; et on peut attendre longtemps avant d'avoir la réponse...
Une petite question: au cours de ces petites délires, je n'ai pas compris pourquoi, par moment il (l'interpreteur) se met à répondre avec des types du genre " '_a->'_b->'c ", sans pour autant que ça l'empèche de fonction ensuite... Le underscore m'a laissé perplexe. J'ai quelques vagues soupçons, mais...
Une autre question: si on a compilé une fonction en camL est-elle ensuite utilisable en l'important dans un autre langage, je veux dire, les types informatiques sont-ils "portables" pour certains (par exemple int->int)?
EDIT: je précise (pour les philosophes) que ci-dessus = "implémentation" des paradoxes classiques de la crise des foncdements (la phrase qui s'affirme elle même fausse)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
oui, on ne te la fait, pas, je me reposais effectivement bien sur camL pour éviter de me prendre la tête sur des "alpha".
Un truc que je rêve un peu de faire (mais ce n'est pas maintenant), c'est de réaliser la contradiction ZF+AC+AD implique tout. Mais il faut déjà que je trouve sous quelle forme j'apprécierai le résultat...
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
En fait, la NBE (normalization by evaluation) c'est beaucoup plus subtil.
On utilise une sémantique d'un certain langage dont les termes normalisent fortement, c'est à dire on a une fonction d'interpretation :
$$[.] : L \rightarrow M$$
Et on cherche une fonction de readback $\rho : M \rightarrow L_n$ où $L_n \subseteq L$ est l'ensemble des termes en forme normale.
Ensuite la normalisation s'écrit juste $norm(t) = \rho([t])$.
En quelque sorte on a plongé naturellement notre terme dans le modèle, et là-dedans pouf, il s'est réduit tout seul, et on le relit.
En fait pour préciser un peu l'orientation de ma "passion" pour ce sujet, il y en 2:
1) prendre un texte écrit presque en langue naturelle, avec des preuves habituelles, le parser, le normaliser, et le renvoyer sous la même forme conviviale. Dans le programme que j'ai fait, hélas, la façon dont le résultat est renvoyée est tellement sale que je ne peux que m'amuser 3 secondes à lire quelques preuves de 3 lignes. La normalisation à priori, bien que je sois d'accord que ça a dû être beaucoup étudié, n'est pas ce qui me soucie le plus (la confluence** règle la question). C'est plutôt la convivialité (ie quelle disposition, comment on entre la preuve (là j'ai choisi le mode "prouveur-sceptique", mais bof bof pour le parsage de preuves déjà scannée) et comment elle ressort ensuite de manière à être aussi "belle"
2) utiliser l'identité pour typer tous les axiomes de ZF à l'exception de "AC" et "extensionnalité" (et là encore trouver une forme sous laquelle renvoyer la preuve normale*** qui soit digeste)
** toi tu le sais je le dis pour tous: "conluence" signifie que quelle que soit la façon (correcte) dont on s'y prend, la preuve normalisée obtenue est la même.
*** si elle existe, bien sûr
Soit dit en passant, peut-être que COQ que je ne connais absolument pas me donnerait peut-être quelques satisfactions, que je n'aie pas à réinventer l'eauc chaude.
à propos de "CallCC": admettons qu'on ait fait une fonction toto:('a->'b)->'a en camL. Y a-t-il un truc tout fait dans camL qui l'envoie sur 'a, du genre qui s'appelle callCC toto: 'a ???
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Pour dff et les autres, je viens de découvrir les exceptions en camL... Je me suis amusé à voir jusqu'où allait la magie du call CC lol. Pas bien loin en fait sur cet exemple.
En tout cas le "tiers exclus" est mis ici en défaut: camL ne peut pas deviner quel élément "magic" de $A\cup (A\to $ est privilégié par le monde platonicien Bon évidemment ça n'étonnera pas les pros, mais... snif, j'aurais bien aimé qu'il me sorte autre chose que "uncaught exception" après m'avoir donné l'illusion que "magic" était dans "union"...
# type my= Z of int;;
type my = Z of int
# exception Leurre of int;;
exception Leurre of int
# let bluf x=raise (Leurre x);;
val bluf : int -> 'a = <fun>
# let gere u v=try u bluf with |Leurre n->v n;;
val gere : ((int -> 'a) -> 'b) -> (int -> 'b) -> 'b = <fun>
# type union=Y of int | W of (int->my);;
type union = Y of int | W of (int -> my)
# let p1 n=Y n;;
val p1 : int -> union = <fun>
# let p2 g=W g;;
val p2 : (int -> my) -> union = <fun>
# let magic = gere p2 p1;;
val magic : union = W <fun>
# let fina q t=match t with
|Y n->n
|W g->let a=g q in (match a with |Z p->p);;
val fina : int -> union -> int = <fun>
# fina 5 magic;;
Uncaught exception: Leurre(5)
# fina 88 magic;;
Uncaught exception: Leurre(88)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Pour les autres lecteurs, je réexplique la "mode" sous-jacente:
la correspondance de Curry Howard transorme (sans effort) les preuves de maths en garanties absolues (du côté informatique: en programmes qui ne bugguent jamais)
Il manquait la "réalisation" du tiers exclus jusqu'aux années 80-90 et un gars (Griffith, je crois ou Griffin) a trouvé que c'était "CallCC" une instruction qui sort des programmes quand ils rencontrent une circonstance particulière.
Traduit dans la vie courante, ça correspond au "bluff honnête" dans le sens suivant:
Si de $A$ vous pouvez déduire $T$ (1)
et si de $A\to B$ vous pouvez aussi déduire $T$ (2)
alors l'axiome du raisonnement par l'absurde vous dit que vous avez le droit d'enchainer en disant "donc $T$"
Pour réaliser ça dans la vie courante, voilà l'astuce: vous faites un chèque (sans provision lol) à un robot (ou un chauffeur de taxi) du montant $A\to B$, en échange de quoi il vous garantit qu'il vous émmène dans le pays $T$. (C'est (2) qui vous donne ce robot ou ce taxi). Il roule (tourne), roule, roule, et vous arrivez dans $T$... ou alors peut-être à un moment, il souhaitera pour mille et une raisons possibles, encaisser votre chèque $A\to B$ avant de continuer (Par exemple, il arrive à une frontière qui exige ce montant pour ouvrir sa barrière)
Dans ce cas, la procédure d'encaissement du chèque est telle que: vous devez FOURNIR A, avant que la banque vous remette B (c'est le sens de "montant $A\to B$)
Du coup, le robot, au moment où il exige d'encaisser le chèque, présente forcément une garantie A: OR c'est là que tout se joue, vous disposez aussi de (1) et donc, vous appuyez sur le bouton "off" du robot, et sortez de votre sac l'autre robt dont vous disposiez qui vous garantit $A\to T$. Vous lui donnez le "A" que vous venez de récupérer et il vous emmène dans $T$. Finalement, sans tricher, vous êtes bien arrivé dans T.
Le programme du post d'avant exploite ça... sans succès lol l'informatque n'ayant pas encore accès au platonisme universel
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Je viens de m'amuser à faire des statistiques avec camL
il y a très peu des théorèmes classiques qui ne sont pas intuitionnistes apparemmet, de l'ordre 1/200 (pour les petites formules). Comme le programme galérait, je l'ai réglé sur pas plus de 8 bouclages et voilà une formule qui est une tautologie et dont je ne sais pas si c'est un théorème intuitionniste lol, les entiers représentent des variables propositionnelles quelconques:
christophe : je suis désolé mais je ne reviens pas vraiment, il reste encore des tonnes de cartons à déballer de mon déménagement, j'ai un entretien mardi et je pars vendredi au japon donner un exposé d'une heure dont je n'ai pas encore fait un slide... Promis, quand j'ai du temps libre je viens te répondre
Allez christophe je me lance. En fait, tu as bien vu, avec les exceptions on peut faire des fonctions de type \verb+'a -> 'b+ :
# exception Exception;;
exception Exception
# let f x = raise Exception;;
val f : 'a -> 'b = <fun>
Or, c'est le cauchemar de tout typeur : si on sais faire cela, alors les types n'ont plus de sens. En post ou pre-composant avec f tu peux donner le type que tu veux à n'importe quelle fonction .
Mais ici l'honneur est sauf, car on ne peut rien faire de cette fonction. Dès que tu veux sortir de l'information d'une exception tu n'as le droit qu'à un seul type. Par exemple :
# let f x = raise Exception;;
val f : 'a -> 'b = <fun>
# exception IntException of int;;
exception IntException of int
# let f x = raise (IntException x);;
val f : int -> 'a = <fun>
# let g x = try f x with IntException y -> y;;
val g : int -> int = <fun>
Donc ce code ne produit aucune erreur, il fait bien du sens, mais il renvoie des entiers.
La situation serait bien différente si on avait le droit à des exception polymorphes. Par exemple :
# exception PolyException of 'a;;
exception PolyException of 'a;;
Mais elles sont proscrites en CAML pour la raison qu'on imagine. Tu peux cependant en trouver dans certains langages fonctionnels...
Bin ne sois pas désolé, et au contraire, merci pour ta réponse, il se trouve que je suis connecté, donc ça tombe bien.
Par contre, je vais mettre un peu de tps à expérimenter tout ça un peu plus tard, en ce moment je bosse (lol), et suis pas trop plongé à m'éclater à tirer sur caml dans tous les sens.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
J'ai mieux compris "raise", mais je ne m'en sers pas souvent, à part pour des expériences...
Voici une autre question assez pimentée.
En camL, on peut construire, à la main, des objets récursifs qui ne sont pas des fonctions, par exemple:
let rec a=3::b and b=7::a
En inventant un nouveau type liste, par exemple:
type liste = Vide | V of int*(liste ref)
se pose une question marrante (ce n'est qu'un exemple) et prise de tête. Comment obtenir une fonction f qui ne boucle pas qui est de type
liste ->(int list)
et qui a la propriété suivante, pour tout m,t,w:
Si m=f(t)
Si t=V(n,r)
Si w=(!r)
alors m=n::(f(w))
Cette question me semble assez cruciale en ce sens que pour tout t, il existe un "f(t)" fabriquable à la main (autrement dit, il existe une fonction récursive f), toujours un peu de ma même manière d'ailleurs, et pourtant, je ne vois pas vraiment comment programmer f
C'est marrant cette limite à priori du langage (sauf si je me gourre et que f se programme facilement)
Intuitivement, on veut une f qui ne boucle pas et qui réponse "au désir":
let rec f t = match t with
|Vide->[ ]
|V(n,r)->let x=(!r) in let m=f x in n::m
Mais bien sûr ces lignes de programmation, qui correspondent au désir, bouclent
Une question récurrente pour DFF (et les autres spéacialistes de camL):
je n'arrive toujours pas à capter comment l'INRIA a implémenté "raise". J'ai fait des expériences en reprogrammant la machine de Krivine, et en faisant la même chose avec le "caml tout fait", je n'obtiens pas les mêmes résultats.
En principe, callcc doit agir comme suit:
[callcc . u] doit executer u après avoir mis sur la pile p l'objet $T_p$
et les $T_q$ s'executent comme suit:
$T_q . v$ remplace la pile courante p par q et exécute $v$
C'est pas ce que semble faire camL...??? :X
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Bon j'exhume ce vieux fil pour poster quelques fichiers. Comme je suis amnésique, je reprogramme tout au lieu de créer des modules, qu'est-ce que ça me saoule ce défaut.
Là je poste un code qui peut être utile. Il cherche une preuve d'une tautologie (si c'en est une et la renvoie sans coupure) en logique classique.
Bon, comme je sais que j'oublirai sous peu que ce fichier "fait ça" et que je m'épuiserai à le refaire à la prochaine occasion, je le mets ici:
[size=x-small]type form = V of int | I of form*form
type strat = Prop of form*strat*strat | Prise of form*strat | H of form
let ip a b= I(a,b)
let rec exis test m=match m with
|[]->false
|x::su->if test x then true else exis test su
let rec foral test m=match m with
|[]->true
|x::su->if (foral test su) then test x else false
let estdans a m=let g x=(x=a) in exis g m
let rec separe m = match m with
|[]->([],[])
|x::su->let (a,b)=separe su in (x::b,a)
let rec melange u v = match u with
|[]->v
|x::su->
(
match v with
|[]->u
|y::re->
if x<y then let w=melange su v in x::w else if x>y then let w=melange u re in y::w else let w=melange su re in x::w
)
let rec tri m=match m with
|[]->[]
|[x]->[x]
|[x;y]->if x<y then m else if x>y then [y;x] else [x]
|_->let (a,b)=separe m in melange (tri a) (tri b)
let estdans a m=let g x=(x=a) in exis g m
let rec vari f=match f with
|V n->if n=0 then [] else [n]
|I(h,c)->(vari h)@(vari c)
let rec varia m=match m with
|[]->[]
|f::su->(vari f)@ (varia su)
let variable m=tri (varia m)
let echec=H(V 0)
let rec eli n so sa = match so with
|H f->if f=V n then sa else so
|Prop(f,u,v)->Prop(f,eli n u sa,eli n v sa)
|Prise(I(h,c),w)->if h=V n then so else Prise(I(h,c),eli n w sa)
let rec stt test f =match f with
|V n->if test n then (H (V n),true) else (H(V n),false)
|I(h,c)->let (sh,bh) = stt test h in let (sc,bc) = stt test c in
(match (bh,bc) with
|(x,true)->(Prise(f,sc),true)
|(false,x)->(Prise(f,sh),true)
|(true,false)->(Prop(f,sh,sc),false)
)
let rec fabrique2 ts mo = match mo with
|[]->(echec,false)
|f::mo2->let (s,b)=stt ts f in if b then (s,true) else fabrique2 ts mo2
let rec fabrique ts me mo = match me with
|[]->fabrique2 ts mo
|f::me2->let (s,b)=stt ts f in if b then fabrique ts me2 mo else (s,true)
let rec chevid m1 m2=match m1 with
|[]->(V 0,false)
|x::m1s->if estdans x m2 then (x,true) else chevid m1s m2
let rec extra m =match m with
|[]->[]
|(V n)::s->n::(extra s)
|f::s->extra s
let rec chdet li me mo = match li with
|[]->let test z=false in (0,false,test)
|x::suite->let (t,b,test2)=chdet suite me mo in
if not(b) then if estdans x me then
let test y=if y=x then true else test2 y in (x,false,test) else if estdans x mo then
let test y=if y=x then false else test2 y in (x,false,test) else (x,true, test2)
else (t,b,test2)
let rec ecri f=match f with
|V n->" " ^ (string_of_int n)
|I(h,c)->"-" ^(ecri h)^ (ecri c)
let rec ecrii m = match m with
|[]->""
|x::suite->(ecri x) ^ "\n" ^(ecrii suite)
let attendre() = let a=read_line() in ()
let rec affiche m n =
print_string ("hypothèses:\n" ^(ecrii m)^"conclusions:\n" ^(ecrii n) ^"\n")
let rec trouver me1 mo1 li=
let (me,mo) = (extra me1,extra mo1) in
let (x,b)=chevid me1 mo1 in if b then (H x,true) else
let (x,b,test)=chdet li me mo in if b then
let (so,bo)=trouver ((V x)::me1) mo1 li in
let (sa,ba)=trouver me1 ((V x)::mo1) li in
if ba then if bo then (eli x so sa,true) else (echec,false) else (echec,false)
else fabrique test me1 mo1
let trouve me mo = let li=variable (me@mo) in trouver me mo li
let rec presente s m n=let (m,n)=((tri m), (tri n)) in
begin
affiche m n ;
match s with
|Prop(I(h,c) as f,s2,s3)->
begin print_string ("choisis" ^ (ecri f) ^"\n"); let a=read_line() in if a="" then presente s2 m (h::n) else presente s3 (c::m) n end
|H f->print_string ("jai gagné " ^ (ecri f) )
|Prise(I(h,c),s2)->
begin print_string ("je prends " ^ (ecri h)^"\n"); attendre(); presente s2 (h::m) (c::n) end
end[/size]
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Ca, c'est le truc qui m'a permis de poster le truc transformé en photo dans le fil bourbaki21.
Il implémente en douceur la théorie des ensembles. J'en avais déjà posté un, mais bêtement j'avais mis le type "bool" aux énoncé ce qui empéchait de les "voir".
[size=x-small]type ens = V of int | Ap of (ens->en) and en = Ip of en*en | Q of (ens->en) | In of ens*ens | Tout
type individu = Set_of of int*enonce |Nom of int and enonce = Appartient of individu*individu | Pourtout of int*enonce | Alors of enonce*enonce |All
let compt=ref 0
let nul()= compt:=0
let dans a b=In(a,b)
let ip u v = Ip(u,v)
let rec verite va jr p=match p with
|Ip(u,v)->if verite va jr u then verite va jr v else true
|Q f->let x=jr f in verite va jr (f x)
|In (b,Ap g)->verite va jr (g b)
|In(b,V n)->va n b
|Tout->false
let vide = let g x=Tout in Ap g
let inclu a b = let g x= Ip (In(x,a), In(x,b) ) in Q g
let et u v = Ip( Ip(u,Ip(v,Tout)),Tout)
let egal a b = et (inclu a b) (inclu b a)
let non u = Ip(u,Tout)
let ou u v =non (et (non u) (non v) )
let union a b=let f x=ou (In(x,a)) (In(x,b)) in Ap f
let existe f = let g x = non (f x) in non (Q g)
let paire a b = let f x=ou (egal x a) (egal x b) in Ap f
let grounion a=let g x z=et (dans x z) (dans z a) in let h x=existe (g x) in Ap h
let parties a= let g x=inclu x a in Ap g
let singleton x=paire x x
let suc x=union x (singleton x)
let rec authenti n=if n<1 then vide else let e=authenti (n-1) in suc e
let stable a=let g x=ip (dans x a) (dans (suc x) a) in Q g
let indu a=et (dans vide a) (stable a)
let entier n= let f a=ip (indu a) (dans n a) in Q f
let grand_n=Ap entier
let grand_r=parties grand_n
let rec deploim a=match a with
|V n->Nom n
|Ap f->
begin incr compt;
let p=(!compt) in let b=V p in Set_of (p,deploi (f b))
end
and deploi t=match t with
|Ip(u,v)->Alors (deploi u,deploi v)
|In(a,b)->Appartient(deploim a,deploim b)
|Tout->All
|Q g->
begin
incr compt;
let p=(!compt) in let b=V p in
Pourtout (p,deploi (g b))
end
let rec ecriture p=match p with
|Appartient(a,b)->(voir a) ^ "$\\in$" ^ (voir b)
|Alors(u,v)->"si " ^ (ecriture u) ^ " alors " ^ (ecriture v)
|Pourtout (n,q)->
let s1=string_of_int n in
let s="$x_{" ^ s1 ^ "}$" in
"pour tout " ^ s ^ "(" ^ (ecriture q) ^ ")"
|All->"tout"
and voir a=match a with
|Nom n->let s1=string_of_int n in "$x_{" ^ s1 ^ "}$"
|Set_of(n,q)->let x=voir (Nom n) in
"ensemble des " ^ x ^ " tels que " ^ (ecriture q)[/size]
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Par exemple, avec le programme d'au dessus, voici ce qu'on obtient comme énoncé pour IN appartient à IR (je ne coche exprès pas la case latex):
curieusement c'est moins lourd que 0 appartient à 3
[size=x-small]ensemble des $x_{13}$ tels que pour tout $x_{14}$(si si si ensemble des $x_{22}$ tels que tout$\in$$x_{14}$ alors si pour tout $x_{15}$(si $x_{15}$$\in$$x_{14}$ alors ensemble des $x_{16}$ tels que si si si si $x_{16}$$\in$$x_{15}$ alors tout alors si si $x_{16}$$\in$ensemble des $x_{17}$ tels que si si si si si si pour tout $x_{21}$(si $x_{21}$$\in$$x_{17}$ alors $x_{21}$$\in$$x_{15}$) alors si pour tout $x_{20}$(si $x_{20}$$\in$$x_{15}$ alors $x_{20}$$\in$$x_{17}$) alors tout alors tout alors tout alors si si si si pour tout $x_{19}$(si $x_{19}$$\in$$x_{17}$ alors $x_{19}$$\in$$x_{15}$) alors si pour tout $x_{18}$(si $x_{18}$$\in$$x_{15}$ alors $x_{18}$$\in$$x_{17}$) alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout$\in$$x_{14}$) alors tout alors tout alors $x_{13}$$\in$$x_{14}$)$\in$ensemble des $x_{1}$ tels que pour tout $x_{2}$(si $x_{2}$$\in$$x_{1}$ alors $x_{2}$$\in$ensemble des $x_{3}$ tels que pour tout $x_{4}$(si si si ensemble des $x_{12}$ tels que tout$\in$$x_{4}$ alors si pour tout $x_{5}$(si $x_{5}$$\in$$x_{4}$ alors ensemble des $x_{6}$ tels que si si si si $x_{6}$$\in$$x_{5}$ alors tout alors si si $x_{6}$$\in$ensemble des $x_{7}$ tels que si si si si si si pour tout $x_{11}$(si $x_{11}$$\in$$x_{7}$ alors $x_{11}$$\in$$x_{5}$) alors si pour tout $x_{10}$(si $x_{10}$$\in$$x_{5}$ alors $x_{10}$$\in$$x_{7}$) alors tout alors tout alors tout alors si si si si pour tout $x_{9}$(si $x_{9}$$\in$$x_{7}$ alors $x_{9}$$\in$$x_{5}$) alors si pour tout $x_{8}$(si $x_{8}$$\in$$x_{5}$ alors $x_{8}$$\in$$x_{7}$) alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout$\in$$x_{4}$) alors tout alors tout alors $x_{3}$$\in$$x_{4}$))[/size]
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Bon, mieux vaut tard que jamais... (depuis que je suis aux 50h c'est dur de passer par Ici...)
Ton incompréhension provient du fait que tu assimiles raise à call/cc.
En fait raise est beaucoup plus limité cela correspond juste au saut sans sauvegarde de pile. C'est assez décevant car on ne peux pas faire des trucs assez chouettes comme des générateurs (par exemple une fonction qui génère les nombres premiers et fait un call/cc après chaque génération pour que tu puisses récupérer quand tu veux le suivant).
Le problème c'est que bien entendu ce n'est pas la machine de Krivine qui evalue caml et que le modèle d' exécution s'y prête très mal. Il y a des compilos ml qui reposent sur une traduction par passage de continuation
et alors tu as ton call/cc gratos.
Ya longtemps que j'ai pas posté quelques petits trucs:
Tout d'avord, en fait j'étais bête, "Callcc" marche très bien sous caml, c'est juste que je faisais pas gaffe au fait que j'exxécutais le truc dans un mode qui ne pouvait pas rattraper toutes les exceptions.
Voic la fonction Callcc
exception Stop
let callcc u =
let r=ref [] in
let bluf x=begin r:=x::(!r); raise(Stop) end in
try u bluf with |Stop ->match (!r) with | x::suite->x;;
et la réponse du compilateur:
val callcc : (('a -> 'b) -> 'a) -> 'a = <fun>
Sinon, au post suivant, je vais mettre (ce qui m'arrive très très rarement) un programme optimisé (enfin légèrement) car ne pas le faire m'a couté que jamais les calculs terminaient (à force de faire récursif sur récursif lool, ça ramait)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Voilà, ça m'arrive pas souvent de faire un truc concret, mais j'en avais besoin.
C'est un programme qui unifie des suites de triplets. On veut que dès que (a,b,c) et (a,y,z) sont rencontrés dans la liste donnée, ça implique que b=y et c=z et de même si (a,b,c) et (x,b,c) sont rencontrés on veut que a=x. Autrement dit, on veut cloturer transitivement par ces conditions et n'avoir qu'un seul nom par classe. Comme ça fait galérer (d'optimiser, j'avais initialement fait un truc à l'arrache), je le partage.
J'en avais besoin pour vérifier un truc qui est le suivant (et qui est très marrant): n'importe quelle preuve prouve n'importe quel énoncé, à condition de rajouter des hypothèses. Bon, mais en fait, il y a une manière canonique de le faire, qui est optimale (ie on ne peut réussir la même chose avec des hypothèses plus faible) et cet outil (ci-dessus) est utilisé.
Voici l'outil.
[size=x-small][color=#0033FF]let rec separe2 m = match m with
|[]->([],[])
|x::su->let (a,b)=separe2 su in (x::b,a)
let rec melange2 u v = match u with
|[]->v
|(a,x)::su->
(
match v with
|[]->u
|(b,y)::re->
if x< y then let w=melange2 su v in (a,x)::w else if x>y then let w=melange2 u re in (b,y)::w else let w=melange2 su re in (a,x)::(b,y)::w
)
let rec tricle2 m=match m with
|[]->[]
|[x]->[x]
|[(a,x);(b,y)]->if x< y then m else if x>y then [(b,y);(a,x)] else [(a,x);(b,y)]
|_->let (a,b)=separe2 m in melange2 (tricle2 a) (tricle2 b)
let rec inverse m=match m with
|[]->[]
|(x,y)::suite->let re = inverse suite in (y,x)::re
let rec tricle1 m = let m2=inverse m in let re=tricle2 m2 in inverse re
let rec actualise m = match m with
|[]->let f x=x in f
|(a,b)::suite->let g=actualise suite in let f x=if x=b then a else g x in f
let rec semantise f li = match li with
|[]->[]
|(a,(x,y))::su->(f a,(f x,f y))::(semantise f su)
let etape liste =
let rep=ref [] in
let aj a b = if a=b then () else if a< b then rep := (a,b)::(!rep) else rep:=(b,a)::(!rep) in
let rec parcours1 m =match m with
|[]->()
|[x]->()
|(a,(b,c))::((x,(y,z))::suite as t)->if a=x then begin aj b y;aj c z;parcours1 t end else parcours1 t
in
let rec parcours2 m = match m with
|[]->()
|[x]->()
|(a,(b,c))::((x,(y,z))::suite as t) ->if (b,c)=(y,z) then begin aj a x; parcours2 t end else parcours2 t
in
begin
let m1 =tricle1 liste in parcours1 m1;
let m2 =tricle2 liste in parcours2 m2;
let r = (!rep) in let nom =
actualise r in (semantise nom liste,r)
end
let rec final li = let (li2,r) = etape li in if r=[] then li2 else final li2
let fina m=let r=final m in tricle1 r
let rec listehas p n = if n< 1 then [] else let m=listehas p (n-1) in (Random.int p,(Random.int p,Random.int p))::m[/color][/size]
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Réponses
(Je suis retombé dessus par hasard, sinon je te l'aurais passé avant).
Oui, je me rappelle: j'allais suivre un cours de Rached sur les formes quadratiques et d'ailleurs c'était très bien ce cours
Merci, et promis.... je vous dirai même mes notes (entre 0,1 et 1,5) et demanderai une photocopie de mes copies pour les poster... je trouve ça rigolo
En fait, j'ai renoncé à m'en occuper (mes excuses aux quelques personnes qui ont pu vouloir m'aider, mais je suis irrécupérable au moins à court terme, et je bosse sur ma psychanalyse.. donc espoir à long terme peut-être),
même si 1mois peut paraitre long, je ne pouvais pas (pour raisons diverses, et persos) tenter une sorte de big focalisation au mois de juin pour tenter le diable et je ne me porte que mieux de ne plus y penser, d'avoir revu mon lycée, etc, bref le quotidien des gens normaux.
Je pense surtout à profiter de "mon addiction" à ce forum pour prendre le tps de réfléchir au programme de maths de l'agreg tout au long de l'an prochain "tranquillement"*** (en espérant ne pas retomber dans de la vélléité maladive) car ça n'a aucun sens de "bourrer" comme ça dans un court délai, non seulement on n'apprend finalement rien mais compte-tenu de ma perception assez perso des maths, j'ai l'impression que les gens dans mon cas désapprennent en se forçant comme des bourrins** (j'ai bien passé quelques soirées début juin dans des bars avec les livres que j'avais achetés, mais le stress me les faisait parcourir trop vite et leur taille m'empéchait de les lire tranquillement (c'est une question d'équilibre).
***Mais faudra que je me force à trainer un peu ds les fils que j'évite systématiquement, genre alg linéaire d'école, analyse d'école, exemples, etc
L'avantage de cette évènement incongru est que j'ai découvert**** camL (voir ci-dessous) et ça m'a donné aussi des "idées" (j'ai découvert qu'existe une forme d'analyse qui a une essence un peu arithmétique (voir fil sur e et pi/2 récent) au détour d'une séance zen où je voulais tenter de me réintéresser à "un programme scolaire" en essayant d'y instiller mes fantasmes (mondes parallèles, voyance, temps, logique)
[size=x-small]**Au bout de quelques heures, je ne voyais plus ce que je lisais et même les écriteaux dans la rue, je ne les comprenais plus, et j'ai ressenti plein de douleurs physiques (psychosomatiques probablement bref... snif, être barjeau a des inconvénients..)[/size]
**** j'y ai passé du tps sur ce langage fascinant, hélas, sans vraie doc, et hélas dans mon environnement PC (j'ai le flemme d'aller sur le CD que j'ai installé... qu'est-ce que je suis con..) avec une fenetre ms dos et de la grosse galère pour exécuter et débugguer
Voici mon programme dont je suis le plus fier:
Tenez-vous bien: il prend un lambda terme, l'exécute intégralement en un terme normal et le tout sans aucun effort, ni "renommage" des variables liées (ce renommage est toujours un truc d'une chiantise absolue, et je voulais le contourner d'une manière élégante... mission accomplie lol, pas un minipet de renommage, 100% bio, 100% métaphysique)
Vous constaterez que le type "tera" ne prévoit même pas la possibilité d'un redex, c'est ça qui me fait le plus kiffer. Quant à l'application "ap", admirez sa concision... Arrrg, c'est dommage que je n'ai pas d'environnement caml convivial pour windows (à la delphi), car je m'éclaterais..
Voici le code:
Je n'ai pas fait d'entrées sorties, mais ça ne saurait tarder
A l'exécution, le programme vous demande ce que vous voulez prouver
Pour entrer un phrase atomique vous rentrer un suite de caractère (évitez parenthèse et crochets)
Pour entrer une implication, vous tapez "-"
ensuite il vous demdande récursivement votre conclusion, puis votre hypothèse
Une fois rentrée votre affirmation, il vous demande de la prouver "à l'envers" (ie vous remontez vers les axiomes de votre choix)
Si à un moment vous voulez prouver A--->B en "supposant A", vous tapez "!"
Si à un moment vous ne souhaitez pas justifier, vous tapez "&"
Si vous souhaitez évoquer une raison (modus ponens), vous tapez D'ABORD n'importe quoi sauf "&","!" (le mieux c'est de taper directement sur "entrée" et là vous entrez votre raison (sur le même mode que vous avez entré votre phrase affirmée de départ
Puis il vous demandera récursivment de prouver raison puis raison ---->votre dernier truc
A la fin, il vous demande dans quel fichier vous souhaitez enregistrer votre preuve et l'y écrit, mais en la normalisant d'abord.
http://www.logique.jussieu.fr/~chalons/deploi.exe
EDIT: je rajoute une précision parce qu'à la relecture je peux sembler sarcastique. Précision : Je ne le suis pas.
Voici un exemple qui ne sert à rien (il fait boucler la machine), mais qui devrait inciter les passionnés de philosophie du forum à ultiliser ce langage:
# type magique = L of (magique->int);;
type magique = L of (magique -> int)
# let pick x=match x with |L(f)->f x;;
val pick : magique -> int = <fun>
# let diag = L(pick);;
val diag : magique = L <fun>
# let entierdivin=pick diag;;
et on peut attendre longtemps avant d'avoir la réponse...
Une petite question: au cours de ces petites délires, je n'ai pas compris pourquoi, par moment il (l'interpreteur) se met à répondre avec des types du genre " '_a->'_b->'c ", sans pour autant que ça l'empèche de fonction ensuite... Le underscore m'a laissé perplexe. J'ai quelques vagues soupçons, mais...
Une autre question: si on a compilé une fonction en camL est-elle ensuite utilisable en l'important dans un autre langage, je veux dire, les types informatiques sont-ils "portables" pour certains (par exemple int->int)?
EDIT: je précise (pour les philosophes) que ci-dessus = "implémentation" des paradoxes classiques de la crise des foncdements (la phrase qui s'affirme elle même fausse)
oui, on ne te la fait, pas, je me reposais effectivement bien sur camL pour éviter de me prendre la tête sur des "alpha".
Un truc que je rêve un peu de faire (mais ce n'est pas maintenant), c'est de réaliser la contradiction ZF+AC+AD implique tout. Mais il faut déjà que je trouve sous quelle forme j'apprécierai le résultat...
On utilise une sémantique d'un certain langage dont les termes normalisent fortement, c'est à dire on a une fonction d'interpretation :
$$[.] : L \rightarrow M$$
Et on cherche une fonction de readback $\rho : M \rightarrow L_n$ où $L_n \subseteq L$ est l'ensemble des termes en forme normale.
Ensuite la normalisation s'écrit juste $norm(t) = \rho([t])$.
En quelque sorte on a plongé naturellement notre terme dans le modèle, et là-dedans pouf, il s'est réduit tout seul, et on le relit.
1) prendre un texte écrit presque en langue naturelle, avec des preuves habituelles, le parser, le normaliser, et le renvoyer sous la même forme conviviale. Dans le programme que j'ai fait, hélas, la façon dont le résultat est renvoyée est tellement sale que je ne peux que m'amuser 3 secondes à lire quelques preuves de 3 lignes. La normalisation à priori, bien que je sois d'accord que ça a dû être beaucoup étudié, n'est pas ce qui me soucie le plus (la confluence** règle la question). C'est plutôt la convivialité (ie quelle disposition, comment on entre la preuve (là j'ai choisi le mode "prouveur-sceptique", mais bof bof pour le parsage de preuves déjà scannée) et comment elle ressort ensuite de manière à être aussi "belle"
2) utiliser l'identité pour typer tous les axiomes de ZF à l'exception de "AC" et "extensionnalité" (et là encore trouver une forme sous laquelle renvoyer la preuve normale*** qui soit digeste)
** toi tu le sais je le dis pour tous: "conluence" signifie que quelle que soit la façon (correcte) dont on s'y prend, la preuve normalisée obtenue est la même.
*** si elle existe, bien sûr
Soit dit en passant, peut-être que COQ que je ne connais absolument pas me donnerait peut-être quelques satisfactions, que je n'aie pas à réinventer l'eauc chaude.
à propos de "CallCC": admettons qu'on ait fait une fonction toto:('a->'b)->'a en camL. Y a-t-il un truc tout fait dans camL qui l'envoie sur 'a, du genre qui s'appelle callCC toto: 'a ???
En tout cas le "tiers exclus" est mis ici en défaut: camL ne peut pas deviner quel élément "magic" de $A\cup (A\to $ est privilégié par le monde platonicien Bon évidemment ça n'étonnera pas les pros, mais... snif, j'aurais bien aimé qu'il me sorte autre chose que "uncaught exception" après m'avoir donné l'illusion que "magic" était dans "union"...
la correspondance de Curry Howard transorme (sans effort) les preuves de maths en garanties absolues (du côté informatique: en programmes qui ne bugguent jamais)
Il manquait la "réalisation" du tiers exclus jusqu'aux années 80-90 et un gars (Griffith, je crois ou Griffin) a trouvé que c'était "CallCC" une instruction qui sort des programmes quand ils rencontrent une circonstance particulière.
Traduit dans la vie courante, ça correspond au "bluff honnête" dans le sens suivant:
Si de $A$ vous pouvez déduire $T$ (1)
et si de $A\to B$ vous pouvez aussi déduire $T$ (2)
alors l'axiome du raisonnement par l'absurde vous dit que vous avez le droit d'enchainer en disant "donc $T$"
Pour réaliser ça dans la vie courante, voilà l'astuce: vous faites un chèque (sans provision lol) à un robot (ou un chauffeur de taxi) du montant $A\to B$, en échange de quoi il vous garantit qu'il vous émmène dans le pays $T$. (C'est (2) qui vous donne ce robot ou ce taxi). Il roule (tourne), roule, roule, et vous arrivez dans $T$... ou alors peut-être à un moment, il souhaitera pour mille et une raisons possibles, encaisser votre chèque $A\to B$ avant de continuer (Par exemple, il arrive à une frontière qui exige ce montant pour ouvrir sa barrière)
Dans ce cas, la procédure d'encaissement du chèque est telle que: vous devez FOURNIR A, avant que la banque vous remette B (c'est le sens de "montant $A\to B$)
Du coup, le robot, au moment où il exige d'encaisser le chèque, présente forcément une garantie A: OR c'est là que tout se joue, vous disposez aussi de (1) et donc, vous appuyez sur le bouton "off" du robot, et sortez de votre sac l'autre robt dont vous disposiez qui vous garantit $A\to T$. Vous lui donnez le "A" que vous venez de récupérer et il vous emmène dans $T$. Finalement, sans tricher, vous êtes bien arrivé dans T.
Le programme du post d'avant exploite ça... sans succès lol l'informatque n'ayant pas encore accès au platonisme universel
il y a très peu des théorèmes classiques qui ne sont pas intuitionnistes apparemmet, de l'ordre 1/200 (pour les petites formules). Comme le programme galérait, je l'ai réglé sur pas plus de 8 bouclages et voilà une formule qui est une tautologie et dont je ne sais pas si c'est un théorème intuitionniste lol, les entiers représentent des variables propositionnelles quelconques:
(((((((9)->14)->11)->(12)->4)->(((12)->10)->((11)->12)->(11)->10)->(((13)->10)->(10)->13)->((14)->4)->10)->((((11)->12)->(14)->10)->(((9)->13)->(11)->12)->(11)->13)->(((11)->14)->(13)->9)->(12)->(9)->14)->(((((12)->4)->(12)->11)->((14)->12)->(13)->10)->((12)->13)->(9)->10)->((((10)->4)->(11)->10)->((11)->12)->14)->(14)->9)->(((((13)->(11)->12)->(((14)->12)->(11)->4)->((10)->11)->(14)->9)->(((13)->(11)->12)->9)->((12)->13)->(9)->4)->((((14)->13)->(12)->11)->((11)->9)->((11)->12)->(9)->14)->(((9)->12)->(14)->11)->((12)->11)->(9)->14)->((((13)->10)->(11)->13)->(11)->9)->((((13)->12)->(12)->9)->((10)->9)->12)->((11)->10)->((10)->14)->(11)->((((13)->10)->(10)->13)->10)->(((12)->(14)->10)->(((9)->13)->12)->13)->((14)->(13)->9)->(12)->(9)->14",
http://www.les-mathematiques.net/phorum/read.php?6,519977,532704#msg-532704
J'avoue que je n'ai réussi à avoir que des traductions anglaises et ne comprend pas comment "raise" interromp ou n'interromp pas les choses
En lien un exemple où j'ai voulu voir
Mais ici l'honneur est sauf, car on ne peut rien faire de cette fonction. Dès que tu veux sortir de l'information d'une exception tu n'as le droit qu'à un seul type. Par exemple : Donc ce code ne produit aucune erreur, il fait bien du sens, mais il renvoie des entiers.
La situation serait bien différente si on avait le droit à des exception polymorphes. Par exemple : Mais elles sont proscrites en CAML pour la raison qu'on imagine. Tu peux cependant en trouver dans certains langages fonctionnels...
Désolé du délai pour ma réponse
Par contre, je vais mettre un peu de tps à expérimenter tout ça un peu plus tard, en ce moment je bosse (lol), et suis pas trop plongé à m'éclater à tirer sur caml dans tous les sens.
Voici une autre question assez pimentée.
En camL, on peut construire, à la main, des objets récursifs qui ne sont pas des fonctions, par exemple:
let rec a=3::b and b=7::a
En inventant un nouveau type liste, par exemple:
type liste = Vide | V of int*(liste ref)
se pose une question marrante (ce n'est qu'un exemple) et prise de tête. Comment obtenir une fonction f qui ne boucle pas qui est de type
liste ->(int list)
et qui a la propriété suivante, pour tout m,t,w:
Si m=f(t)
Si t=V(n,r)
Si w=(!r)
alors m=n::(f(w))
Cette question me semble assez cruciale en ce sens que pour tout t, il existe un "f(t)" fabriquable à la main (autrement dit, il existe une fonction récursive f), toujours un peu de ma même manière d'ailleurs, et pourtant, je ne vois pas vraiment comment programmer f
C'est marrant cette limite à priori du langage (sauf si je me gourre et que f se programme facilement)
Intuitivement, on veut une f qui ne boucle pas et qui réponse "au désir":
let rec f t = match t with
|Vide->[ ]
|V(n,r)->let x=(!r) in let m=f x in n::m
Mais bien sûr ces lignes de programmation, qui correspondent au désir, bouclent
je n'arrive toujours pas à capter comment l'INRIA a implémenté "raise". J'ai fait des expériences en reprogrammant la machine de Krivine, et en faisant la même chose avec le "caml tout fait", je n'obtiens pas les mêmes résultats.
En principe, callcc doit agir comme suit:
[callcc . u] doit executer u après avoir mis sur la pile p l'objet $T_p$
et les $T_q$ s'executent comme suit:
$T_q . v$ remplace la pile courante p par q et exécute $v$
C'est pas ce que semble faire camL...??? :X
Callcc fait ça (en langage informel):
pop (u) ; a:=pile ; push (T(a)) ; execute u
et T(q) fait ça:
pop (v) ; remplace la pile par q ; execute v
(où "execute" veut juste dire "passe le relais à")
Là je poste un code qui peut être utile. Il cherche une preuve d'une tautologie (si c'en est une et la renvoie sans coupure) en logique classique.
Bon, comme je sais que j'oublirai sous peu que ce fichier "fait ça" et que je m'épuiserai à le refaire à la prochaine occasion, je le mets ici:
[size=x-small]type form = V of int | I of form*form
type strat = Prop of form*strat*strat | Prise of form*strat | H of form
let ip a b= I(a,b)
let rec exis test m=match m with
|[]->false
|x::su->if test x then true else exis test su
let rec foral test m=match m with
|[]->true
|x::su->if (foral test su) then test x else false
let estdans a m=let g x=(x=a) in exis g m
let rec separe m = match m with
|[]->([],[])
|x::su->let (a,b)=separe su in (x::b,a)
let rec melange u v = match u with
|[]->v
|x::su->
(
match v with
|[]->u
|y::re->
if x<y then let w=melange su v in x::w else if x>y then let w=melange u re in y::w else let w=melange su re in x::w
)
let rec tri m=match m with
|[]->[]
|[x]->[x]
|[x;y]->if x<y then m else if x>y then [y;x] else [x]
|_->let (a,b)=separe m in melange (tri a) (tri b)
let estdans a m=let g x=(x=a) in exis g m
let rec vari f=match f with
|V n->if n=0 then [] else [n]
|I(h,c)->(vari h)@(vari c)
let rec varia m=match m with
|[]->[]
|f::su->(vari f)@ (varia su)
let variable m=tri (varia m)
let echec=H(V 0)
let rec eli n so sa = match so with
|H f->if f=V n then sa else so
|Prop(f,u,v)->Prop(f,eli n u sa,eli n v sa)
|Prise(I(h,c),w)->if h=V n then so else Prise(I(h,c),eli n w sa)
let rec stt test f =match f with
|V n->if test n then (H (V n),true) else (H(V n),false)
|I(h,c)->let (sh,bh) = stt test h in let (sc,bc) = stt test c in
(match (bh,bc) with
|(x,true)->(Prise(f,sc),true)
|(false,x)->(Prise(f,sh),true)
|(true,false)->(Prop(f,sh,sc),false)
)
let rec fabrique2 ts mo = match mo with
|[]->(echec,false)
|f::mo2->let (s,b)=stt ts f in if b then (s,true) else fabrique2 ts mo2
let rec fabrique ts me mo = match me with
|[]->fabrique2 ts mo
|f::me2->let (s,b)=stt ts f in if b then fabrique ts me2 mo else (s,true)
let rec chevid m1 m2=match m1 with
|[]->(V 0,false)
|x::m1s->if estdans x m2 then (x,true) else chevid m1s m2
let rec extra m =match m with
|[]->[]
|(V n)::s->n::(extra s)
|f::s->extra s
let rec chdet li me mo = match li with
|[]->let test z=false in (0,false,test)
|x::suite->let (t,b,test2)=chdet suite me mo in
if not(b) then if estdans x me then
let test y=if y=x then true else test2 y in (x,false,test) else if estdans x mo then
let test y=if y=x then false else test2 y in (x,false,test) else (x,true, test2)
else (t,b,test2)
let rec ecri f=match f with
|V n->" " ^ (string_of_int n)
|I(h,c)->"-" ^(ecri h)^ (ecri c)
let rec ecrii m = match m with
|[]->""
|x::suite->(ecri x) ^ "\n" ^(ecrii suite)
let attendre() = let a=read_line() in ()
let rec affiche m n =
print_string ("hypothèses:\n" ^(ecrii m)^"conclusions:\n" ^(ecrii n) ^"\n")
let rec trouver me1 mo1 li=
let (me,mo) = (extra me1,extra mo1) in
let (x,b)=chevid me1 mo1 in if b then (H x,true) else
let (x,b,test)=chdet li me mo in if b then
let (so,bo)=trouver ((V x)::me1) mo1 li in
let (sa,ba)=trouver me1 ((V x)::mo1) li in
if ba then if bo then (eli x so sa,true) else (echec,false) else (echec,false)
else fabrique test me1 mo1
let trouve me mo = let li=variable (me@mo) in trouver me mo li
let rec presente s m n=let (m,n)=((tri m), (tri n)) in
begin
affiche m n ;
match s with
|Prop(I(h,c) as f,s2,s3)->
begin print_string ("choisis" ^ (ecri f) ^"\n"); let a=read_line() in if a="" then presente s2 m (h::n) else presente s3 (c::m) n end
|H f->print_string ("jai gagné " ^ (ecri f) )
|Prise(I(h,c),s2)->
begin print_string ("je prends " ^ (ecri h)^"\n"); attendre(); presente s2 (h::m) (c::n) end
end[/size]
Il implémente en douceur la théorie des ensembles. J'en avais déjà posté un, mais bêtement j'avais mis le type "bool" aux énoncé ce qui empéchait de les "voir".
[size=x-small]type ens = V of int | Ap of (ens->en) and en = Ip of en*en | Q of (ens->en) | In of ens*ens | Tout
type individu = Set_of of int*enonce |Nom of int and enonce = Appartient of individu*individu | Pourtout of int*enonce | Alors of enonce*enonce |All
let compt=ref 0
let nul()= compt:=0
let dans a b=In(a,b)
let ip u v = Ip(u,v)
let rec verite va jr p=match p with
|Ip(u,v)->if verite va jr u then verite va jr v else true
|Q f->let x=jr f in verite va jr (f x)
|In (b,Ap g)->verite va jr (g b)
|In(b,V n)->va n b
|Tout->false
let vide = let g x=Tout in Ap g
let inclu a b = let g x= Ip (In(x,a), In(x,b) ) in Q g
let et u v = Ip( Ip(u,Ip(v,Tout)),Tout)
let egal a b = et (inclu a b) (inclu b a)
let non u = Ip(u,Tout)
let ou u v =non (et (non u) (non v) )
let union a b=let f x=ou (In(x,a)) (In(x,b)) in Ap f
let existe f = let g x = non (f x) in non (Q g)
let paire a b = let f x=ou (egal x a) (egal x b) in Ap f
let grounion a=let g x z=et (dans x z) (dans z a) in let h x=existe (g x) in Ap h
let parties a= let g x=inclu x a in Ap g
let singleton x=paire x x
let suc x=union x (singleton x)
let rec authenti n=if n<1 then vide else let e=authenti (n-1) in suc e
let stable a=let g x=ip (dans x a) (dans (suc x) a) in Q g
let indu a=et (dans vide a) (stable a)
let entier n= let f a=ip (indu a) (dans n a) in Q f
let grand_n=Ap entier
let grand_r=parties grand_n
let rec deploim a=match a with
|V n->Nom n
|Ap f->
begin incr compt;
let p=(!compt) in let b=V p in Set_of (p,deploi (f b))
end
and deploi t=match t with
|Ip(u,v)->Alors (deploi u,deploi v)
|In(a,b)->Appartient(deploim a,deploim b)
|Tout->All
|Q g->
begin
incr compt;
let p=(!compt) in let b=V p in
Pourtout (p,deploi (g b))
end
let rec ecriture p=match p with
|Appartient(a,b)->(voir a) ^ "$\\in$" ^ (voir b)
|Alors(u,v)->"si " ^ (ecriture u) ^ " alors " ^ (ecriture v)
|Pourtout (n,q)->
let s1=string_of_int n in
let s="$x_{" ^ s1 ^ "}$" in
"pour tout " ^ s ^ "(" ^ (ecriture q) ^ ")"
|All->"tout"
and voir a=match a with
|Nom n->let s1=string_of_int n in "$x_{" ^ s1 ^ "}$"
|Set_of(n,q)->let x=voir (Nom n) in
"ensemble des " ^ x ^ " tels que " ^ (ecriture q)[/size]
curieusement c'est moins lourd que 0 appartient à 3
[size=x-small]ensemble des $x_{13}$ tels que pour tout $x_{14}$(si si si ensemble des $x_{22}$ tels que tout$\in$$x_{14}$ alors si pour tout $x_{15}$(si $x_{15}$$\in$$x_{14}$ alors ensemble des $x_{16}$ tels que si si si si $x_{16}$$\in$$x_{15}$ alors tout alors si si $x_{16}$$\in$ensemble des $x_{17}$ tels que si si si si si si pour tout $x_{21}$(si $x_{21}$$\in$$x_{17}$ alors $x_{21}$$\in$$x_{15}$) alors si pour tout $x_{20}$(si $x_{20}$$\in$$x_{15}$ alors $x_{20}$$\in$$x_{17}$) alors tout alors tout alors tout alors si si si si pour tout $x_{19}$(si $x_{19}$$\in$$x_{17}$ alors $x_{19}$$\in$$x_{15}$) alors si pour tout $x_{18}$(si $x_{18}$$\in$$x_{15}$ alors $x_{18}$$\in$$x_{17}$) alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout$\in$$x_{14}$) alors tout alors tout alors $x_{13}$$\in$$x_{14}$)$\in$ensemble des $x_{1}$ tels que pour tout $x_{2}$(si $x_{2}$$\in$$x_{1}$ alors $x_{2}$$\in$ensemble des $x_{3}$ tels que pour tout $x_{4}$(si si si ensemble des $x_{12}$ tels que tout$\in$$x_{4}$ alors si pour tout $x_{5}$(si $x_{5}$$\in$$x_{4}$ alors ensemble des $x_{6}$ tels que si si si si $x_{6}$$\in$$x_{5}$ alors tout alors si si $x_{6}$$\in$ensemble des $x_{7}$ tels que si si si si si si pour tout $x_{11}$(si $x_{11}$$\in$$x_{7}$ alors $x_{11}$$\in$$x_{5}$) alors si pour tout $x_{10}$(si $x_{10}$$\in$$x_{5}$ alors $x_{10}$$\in$$x_{7}$) alors tout alors tout alors tout alors si si si si pour tout $x_{9}$(si $x_{9}$$\in$$x_{7}$ alors $x_{9}$$\in$$x_{5}$) alors si pour tout $x_{8}$(si $x_{8}$$\in$$x_{5}$ alors $x_{8}$$\in$$x_{7}$) alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout alors tout$\in$$x_{4}$) alors tout alors tout alors $x_{3}$$\in$$x_{4}$))[/size]
Ton incompréhension provient du fait que tu assimiles raise à call/cc.
En fait raise est beaucoup plus limité cela correspond juste au saut sans sauvegarde de pile. C'est assez décevant car on ne peux pas faire des trucs assez chouettes comme des générateurs (par exemple une fonction qui génère les nombres premiers et fait un call/cc après chaque génération pour que tu puisses récupérer quand tu veux le suivant).
Le problème c'est que bien entendu ce n'est pas la machine de Krivine qui evalue caml et que le modèle d' exécution s'y prête très mal. Il y a des compilos ml qui reposent sur une traduction par passage de continuation
et alors tu as ton call/cc gratos.
Tout d'avord, en fait j'étais bête, "Callcc" marche très bien sous caml, c'est juste que je faisais pas gaffe au fait que j'exxécutais le truc dans un mode qui ne pouvait pas rattraper toutes les exceptions.
Voic la fonction Callcc
exception Stop
let callcc u =
let r=ref [] in
let bluf x=begin r:=x::(!r); raise(Stop) end in
try u bluf with |Stop ->match (!r) with | x::suite->x;;
et la réponse du compilateur:
val callcc : (('a -> 'b) -> 'a) -> 'a = <fun>
Sinon, au post suivant, je vais mettre (ce qui m'arrive très très rarement) un programme optimisé (enfin légèrement) car ne pas le faire m'a couté que jamais les calculs terminaient (à force de faire récursif sur récursif lool, ça ramait)
C'est un programme qui unifie des suites de triplets. On veut que dès que (a,b,c) et (a,y,z) sont rencontrés dans la liste donnée, ça implique que b=y et c=z et de même si (a,b,c) et (x,b,c) sont rencontrés on veut que a=x. Autrement dit, on veut cloturer transitivement par ces conditions et n'avoir qu'un seul nom par classe. Comme ça fait galérer (d'optimiser, j'avais initialement fait un truc à l'arrache), je le partage.
J'en avais besoin pour vérifier un truc qui est le suivant (et qui est très marrant): n'importe quelle preuve prouve n'importe quel énoncé, à condition de rajouter des hypothèses. Bon, mais en fait, il y a une manière canonique de le faire, qui est optimale (ie on ne peut réussir la même chose avec des hypothèses plus faible) et cet outil (ci-dessus) est utilisé.
Voici l'outil.