blogs@iaddg.net

Reader

Read the latest posts from blogs@iaddg.net.

from Logic & Programming

По покана на Филозофското друштво на Македонија и Институтот за филозофија при УКИМ, на 13. јануари 2024 одржав предавање на Зум со следнава содржина:

Во ова предавање ќе ги објасниме феномените на комплетност и на некомплетност на формалните логички системи, од нивната историска генеза, преку теоремите на Гедел и на Кирби-Парис, па сѐ до некои од перспективите кои овие резултати ги отвориле или ги оставиле отворени до денешен ден.

Линк до слајдовите: https://iaddg.net/danko/den-na-logikata-2024.pdf

Видеото онлајн: https://blog.iaddg.net/dash/sdl2024/

Видеото за симнување преку торент: https://iaddg.net/danko/sdl2024.torrent

 
Прочитај повеќе...

from Logic & Programming

by Kawano, Tomoaki; Matsuda, Naosuke; Takagi, Kento

The paper studies the equivalence of intuitionistic and classical validity in propositional logic for a language that contains as the only logicial connectives the ones that represent monotonic Boolean formulas.

It is shown that, for this class of formulas, intuitionistic and classical validity coincide. The notion of classical validity is the usual one (sometimes called Tarski semantics), while, for the notion of intuitionistic validity, the authors use what they call extended Kripke interpretation: the interpretation consists in, for every connective, prefixing a universal quantification $v\ge w$ (meaning ``in a possible world $v$ extending the world $w$'') before the classical interpretation of the connective.

The result is interesting, because usually intuitionistic and classical validity are shown to coincide for classes of formulas such as the so called “negative” formulas (that exclude the authentically intuitionistic connectives of disjunction and existential quantification). The class of monotone Boolean formulas thus in a way generalizes the class of negative ones.

The result shown is said to answer an open question posed by van der Giessen about the proof theory of inuitionistic and classical natural deduction calculi, however in the paper the link between the model theory developed in the paper and the proof theory of the open question is not made in sufficient detail (is there a soundness and completeness theorem for the notion of validity used with respect to the calculi?).

 
Read more...

from Logic & Programming

My PhD student Wendlasida Ouedraogo defended his PhD thesis on Source code optimization for safety critical software at the École Polytechnique in Palaiseau.

He showed how to do provably correct transformations of source-code for a fragment of the Ada language, used in real-world critical software, inside the Coq proof assistant. Using such transformations, one can optimize programs at the entry of a compiler, and does not pose the burden on proving simulation theorems between various compiler intermediate languages, like it is usually done (ex. in CompCert).

He also developed a tool-chain to write provably correct lexers, CoqLex, lexing previously being a compiling phase that was not done formally.

Congratulations and the best of luck to Wendlasida!

 
Read more...

from Logic & Programming

This book shows how to formalize some very basic mathematical notions from Logic, Abstract Algebra, Analysis, Linear Algebra, Differential Equations and Probability Theory, inside the functional programming language Haskell. Haskell is appropriate for expressing such notions since it encourages the use of high-order functions (resulting in concise, category-theory-like formulations), its variables are immutable (just like in Mathematics, eliminating computational side-effects related to variable mutation in imperative programming languages), it has algebraic data types (allowing inductive/recursive formulations and reasoning), and type classes (useful for treating mathematical theories in a compositional way). These same features are shared by proof assistant software such as Coq, which have been used extensively for formalization of Mathematics, however, what is different in the approach of this book, with respect to formalization efforts in settings with richer type systems, is that it allows one to build up an abstract mathematical concept more rapidly and experiment with it computationally, making it an interesting setting for doing experimental mathematics.

The book could be useful (indeed, it started as a coursebook for undergraduate students) for Mathematics students studying functional programming or Computer Science students studying Mathematics, but it could also be useful for researchers learning how to efficiently formalize their favorite mathematical theory inside a proof assistant. The formulations of the exponential function, the Laplace transform and the “axiomatization” of probability are elegant (concise!). One could perhaps regret the absence of definition of real numbers in the framework (real numbers are treated abstractly).

 
Read more...

from GR7

Blason

O doux cheveux blonds, ô soyeuses mèches, Tant vous me rendez heureux, qu’ à vous voir, Dans mon cœur se crée une grande brèche, Que sans vous toucher tout n'est que déboire.

O belles mains, ô paumes d’un blanc neige, Tant vous m’envoûtez, qu’à vous caresser, Me vient l’envie, tombé dans votre piège, De bijoux vous couvrir pour vous flatter.

Tant de plaisir à vous considérer, Tant d'amour, de désir me vient en tête, Que si jamais ne puis vous cajoler, M'enterreront avec ce sombre en-tête:

Mort, de n'avoir pu aimer.

 
Lire la suite...

from GR7

5 décembre 1540 Aujourd’hui, j’ai décidé de commencer à écrire ce journal. L’idée m’est venue à l’esprit, lorsque je me suis rendu compte que, dans mes poèmes, je ne pouvais pas être totalement sincère avec mes lectrices, d'où l’envie d’un confident, à qui je puisse livrer tous mes sentiments. Quoi de mieux, donc, comme confesseur, qu’un journal intime. Mais il y a une bonne raison au fait que j’ai choisi de rédiger ce carnet justement aujourd’hui, en ce 5 décembre 1540. Et cette raison, c’est que demain je dois rencontrer mon potentiel, futur mari, Ennemond Perrin. Ennemond Perrin est un riche marchand de cordes qui possède plusieurs maisons à Lyon. Mon père essaye d’arranger le mariage pour des motifs flagrants : la richesse et les propriétés de Monsieur Perrin. Ces derniers m’assureraient un avenir financier stable et surtout, plus important pour moi encore, un moyen de satisfaire ma passion pour les lettres. Je devrais donc être radieuse devant la perspective de cette rencontre prometteuse qui mènera sans doute à une alliance qui l’est tout autant. Ce serait d’ailleurs le cas s’il n’y avait pas un élément qui se mettait au travers de ma bonne volonté. Je suis amoureuse d’un autre homme. Mon amant se nomme Pierre de Fontenais, je l’ai rencontré après mon retour du couvent de la Déserte, lors d’une de ces nombreuses soirées de lecture que j’organisais avant que mon père me les interdise, jugeant que j’y perdais mon temps. La beauté de Pierre n’a pour égale que son intelligence, qui lui a permis d’intégrer les cercles littéraires les plus restreints de Lyon. Dès notre première rencontre, ce fUt le coup de foudre amoureux, notre attrait pour les lettres nous rendant inséparables. Pendant un an nous vécûmes le parfait amour, un an jonché de tendres baisés et de douces caresses, et nous serions déjà mariés à l’heure qu’il est, si mon père ne m’avait interdit de le côtoyer, déclarant qu’il n’était pas assez sérieux et surtout n’avait pas la fortune qui me contenterait. Ainsi nous continuâmes à nous voir en cachette, la nuit tombée, attendant de trouver une solution à notre malheur. Tout cela jusqu’à aujourd’hui, jour funeste où je vais devoir lui annoncer que je vais sans nul doute me marier avec un autre, et que je vais rencontrer cet autre demain.

6 décembre 1540 Avant de parler de ma rencontre avec monsieur Perrin, je dois absolument te faire part, cher carnet, de mon entrevue avec Pierre. M’étant moi-même réduite à accepter mon triste sort, j’ai dû également me préparer à affronter le moment où j’apprendrais à Pierre la nouvelle de mon mariage. Tout cela pesant sur mon moral, c’est donc en larmes que je me suis dirigée, accompagnée d’une de mes servantes, vers le logement de mon amant. Il habite une auberge rue Mercière et me voyant arriver chez lui en pleurs, il me fIt un accueil de baisers et de tendresses. Il ne comprenait pas ce qui se passait et ce n’est que lorsque je fus installée, bien au chaud, un verre de vin à la main, et lui m’enlaçant dans ses bras, que je lui appris la triste nouvelle, j’allais sans doute me marier. Il y eut un long silence. Je crus mourir d’angoisse devant cette réaction. Puis enfin, d’un air calme, il dit : « Enfuyons-nous. » Au début j’étais sceptique, j’avais peur devant cette perspective de fuite, mais peu à peu, de véritables projets se sont mis en place. Pierre y réfléchissait depuis longtemps, suite aux interdictions de mon père, il avait concocté tout un plan afin que nous puissions être libres de vivre notre amour, il n’avait jamais osé le mettre en œuvre, mais à présent le moment était venu. C’est ainsi que nous décidâmes que dans deux jours, aux premières lueurs de l’aube, il viendrait me chercher et que nous partirions chez son oncle qui habite Pérouges. Je suis si contente à l’idée de cette aventure, que j’en ris rien que d’y penser. Imagine, cher journal, que dans deux jours je vivrai le parfait amour avec le parfait amant. Passons mon bonheur, je vais à présent te révéler ce qui s’est passé lors de ma visite chez Monsieur Perrin, quoiqu’il n’y ait, en fin de compte, pas grand-chose à révéler. Ce fût une rencontre, somme toute, ordinaire, en dehors du fait qu’elle eut pour but de sceller mon destin si je n’avais pas décidé de fuir avec Pierre. Nous partîmes tôt, moi, ma mère et mon père pour paraître à 18 heures chez Monsieur Perrin qui habite une immense demeure au nord de Lyon. Arrivés, nous prîmes le souper, discutâmes de tout et de rien et mon père essaya de toucher un mot du mariage à la famille du garçon. Ce dernier est un jeune homme d’à peu près mon âge, quoiqu’il ait un air plus lassé et bien plus mou que le mien. Son visage ne m’est pas trop désagréable, mais il ne me procure pas la même attirance que celui de Pierre, loin de là. Et pour ne pas arranger les choses, monsieur Perrin ne m’a pas l’air d’être un homme de lettres, en effet, au vu des quelques paroles que nous avons échangées au cours du repas, il m’a semblé bien plus intéressé par la corderie que par toute autre chose. Comprends donc cher confident que je n’accorde pas une grande importance à cette rencontre, d’autant plus qu’elle n’aboutira à rien puisque je vais quitter Lyon avec Pierre dès demain.

7 décembre 1540 Je n’arrive pas à y croire. Pierre est mort. Ne le voyant pas arriver ce matin j’ai décidé d’aller voir chez lui ce qui se passait et quelle était la cause de son retard. Je suis donc parti, toute seule, à travers cette froide matinée de décembre en direction de la rue Mercière. En arrivant devant l’auberge où habite Pierre, je vis un attroupement autour de ce qui me semblait être son cheval. Ne pouvant pas passer à cause de la foule, j’ai demandé à un passant ce qui se passait, il m’a répondu qu’un jeune homme voulant monter sur son cheval avait glissé à cause du verglas et tombant de la sorte, avait sans doute agrippé sa monture pour se retenir, ce dernier dans la panique du moment lui avait prodigué un terrible coup de sabot qui en plus de le sonner, avait aggravé sa chute et l’avait fait tomber directement sur la tête. Son état paraissait désespéré. C’est là que je compris. Je me pressai à travers la foule, je bousculai les passants, criant pour qu’on me laisse passer et, arrivant enfin au centre du cercle, j’eus juste le temps de voir le prêtre, appelé pour l’occasion, fermer les yeux de Pierre, prononçant ce jugement : « Ce jeune homme est mort, paix à son âme. » Je crus mourir, je m’évanouis. À présent je suis chez moi, un des membres de l’attroupement m’ayant reconnue et ramenée. Je ne sais plus où j’en suis et n’ai même plus la force de pleurer. Comme je l’ai dit dans un de mes poèmes : « Puis quand je crois ma joie être certaine Et être au haut de mon désiré heur, Il me remet en mon premier malheur. »

 
Lire la suite...