Recherche:

Je relance ce topic!
Dr Topos, tu nous avais promis une petite explication sur les sommes... 8-)

On peut dire qu'il existe un unique booléen b tel que [x > Vrai, y > Faux]b=Vrai?
On peut donc utiliser l'opérateur de description?

pff je nage.
Comment construire un r alors qu'on a pas d'opérateur de construction pour les types O?
C'est encore un peu flou pour moi ce qu'est une proposition.
Est-ce que x=Bvrai est une...

Bon, je tente:
q:O |-> p:W(!1x:Boole q) |-> #(p)
Mais c'est juste pour dire une connerie ;)

Comment utilise t'on l'opérateur de description? Que décrit-il?
Si j'ai bien compris, il donne la valeur de x fesant que E est vrai:
x=#(p) avec p = W(!1x:T E)

Comment l'utilise t-on dans la...

Dans les ensembles: l'union disjointe
Dans les types: la somme "à la CAML"
Dans les énoncés: le "ou"

Voila. Pour le PGCD, je crois que je suis bien incapable de le démontrer...

OK, je croyais qu'une application transformait un ensemble en un autre.
Elle transforme plutôt un élément de l'ensemble de départ en un élément de l'ensemble d'arrivée.

Dans le cas du singleton,...

Daccord, il faut un

et

A et B étant les buts m tel que n divise m, n, m appartiennent à N+.

Mais je n'ai pas très bien compris comment on trouve un objet final:

Comment on montre ça?...

Bon, il reste (1,1).
Il y a un seul objet final dans la catégorie, ce qui n'est pas très utile.
Il n'y a donc pas de produit?

Si je reprend les définitions:



Il me semble que les seuls objets qui n'ont qu'une seule flèche qui pointe vers eux sont les nombres premiers.

les n = tous les entiers naturels strictement...

Dans les ensembles: le produit cartésien
Dans les types: l'aggrégation, la structure
Dans les énoncés: le "et" ?

Pour le question 26 il faut utiliser une conditionnelle aussi?
On pourrait construire le type somme des propositions vrai et des propositions fausses.
A cause du tiers exclus, ce type somme = O....

Je regarde la


Par réciproque on entend ~f ?
Si c'est le cas je dirais intuitivement
(a:Boole) |-> [x > vrai, y > faux](a)
En inversant vrai et faux.
On voit bien qu'on aura toujours f|~f...

C'est vrai que la notation [x > E, y > F](a) m'a beaucoup perturbé, surtout parceque on dirait qu'on compare 2 choses de types différents avec le symbole ">".
Ce qui m'embète encore c'est qu'on...

Je comprend mieux ce qu'est un contexte. J'aurais du percuter plus tôt, c'est comme un contexte en C par exemple (avec les notions de porté et de visibilité)... Je vais vraiment chercher 12h à 14h......

La règle D2! Justement celle que j'ai le moins compris :mouarf:


Je n'ai pas très bien compris ce qu'est un contexte. C'est juste un ensemble de types?
Γ(x:T) C'est un contexte augmenté d'un...

Je développe juste un cran de plus:
Bfaux:Boole |-> q:O |-> q
et
Bvrai:Boole |-> q:O |-> x:W(q) |-> q
Pour aller plus loin, il faudrait utiliser un genre de projection (p1 et p2)?

Je regarde cette question. J'avoue que je n'ai pas très bien compris ce qu'est la somme de types. Pour le produit cartésien, je vois, cela correspond grosso modo à une structure.
Mais une somme?...

Superbe!

Steki-kun pourrait-tu m'expliquer:



Ton terme est une fonction qui prend un énoncé q, une preuve de q et de non q, ce qui effectivement est absurde...
Mais ensuite comment combine tu deux...

Je tente la question 15. Mes maths sont bien rouillés, mais le ridicule ne tue pas ;) En m'inspirant du post #17 :

le type W(?q:O (q => ~~q)) est équivalent à
(q:O) -> W( q => ~~q).
qui est...

Effectivement,
un refactoring peut être vu comme une suite d'opérations élémentaires appliquées à un programme.
Si ces opérations sont certifiées "invariants sémantiques", elles peuvent être...

Je pensais plutôt à un refactoring manuel.
Dans mon métier d'informaticien, on est souvent amené à faire des refactoring, comme par exemple de déplacer des traitements d'un package à l'autre.
Les...

OK, patience, patience... ;)
Une question ma turlupine quand même. Je la pose ici, mais si tu le préfère je la déplace dans l'autre fils, les 2 sujets sont proches:
Si je comprend bien, un...

Salut à tous,
Je me passionne pour ce fils.
Mais j'avoue que depuis la page 3-4, j'ai décroché et je n'arrive plus à raccrocher :))

Je n'ai plus trop l'habitude des maths, donc il m'a fallut...