Short paper on hydra-battles

Casteran commented 3 years ago

@palmskog @cpitclaudel @start974 @Zimmi48

We think that the JFLA (French speaking workshop on functional languages (http://jfla.inria.fr/jfla2022.html) would be a nice opportunity to present the current state and evolution of hydra-battles.

The accompanying article may be written in English (8 pages). We would be very glad if this paper were co-authored by the five of us.

It looks like the following points should be addressed:

New contents since the 2018 talk (https://hal.inria.fr/hal-01707376/document, pp. 91-104)
influence of the coq-community eco-system on the library (e.g. Ackermann, Gaia), maintenance and CI
Documentation with Alectryon
???

A draft is on the branch jfla2022 (in doc/FFLA2022/) Please tell us if you agree with this project.

Pierre and Théo

Next Friday, we will have a meeting in Bordeaux for working about this paper.

palmskog commented 3 years ago

@Casteran @Zimmi48 this project looks good to me, and I would be happy to be a co-author. Unfortunately I can't read technical French to understand in detail the previous submission, but I think I could help out with writing the new submission with some high-level direction. I also hope I can participate in the meeting remotely or synchronize with Théo afterwards.

Casteran commented 3 years ago

Thanks! We will submit this paper in English (only the talk must be in French). The draft is already written in (still poor !) English on doc/JFLA2022/paper.tex

Le 20 sept. 2021 à 14:50, Karl Palmskog @.***> a écrit :

@Casteran https://github.com/Casteran @Zimmi48 https://github.com/Zimmi48 this project looks good to me, and I would be happy to be a co-author. Unfortunately I can't read technical French to understand in detail the previous submission, but I think I could help out with writing the submission with some high-level direction. I also hope I can participate in the meeting remotely or synchronize with Théo afterwards.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/82#issuecomment-922897646, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCS6NHB462OGOC6JSYLUC4UZ5ANCNFSM5ELXOA4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

Casteran commented 3 years ago

@palmskog Sorry, I misunderstood the reference to the previous submission.

Indeed, the previous submission (in French) contained some material now contained in the book

formal descrition of the rules of the Hydra battles (representation in Coq).
Proof of termination of all hydra battles
Some Ketonen-Solovay stuff, and a proof that no measure mapping hydras to a segment [0,mu), where mu<epsilon0 can prove the termination of all hydra battles.
the 2018 article ended with a remark : in the last proof, we used the possibility that the hydra could chose freely its number of new copies at every step of the game, while most presentations of the game restrict this number : i copies at step i. Thus one may wonder if this theorem is still provable when we consider this restriction. For this purpose, new Ketonen-Solovay stuff has been added to the development. Still considering this restriction (which I call "standard" battles in the book), I also study the number of steps of a battle, and prove that this number cannot be returned by any primitive recursive function (given a hydra h, and depending on the initial number of copies).

palmskog commented 3 years ago

@Casteran thanks a lot for the summary! It was clear to me that current version was to be written in English (I've read English papers in JFLA proceedings before).

Let me add one piece of related work that we should probably discuss in the new paper: the undecidable problems library from Saarland. This library also has a formalization of Peano arithmetic, first-order logic, and primitive recursive functions.

palmskog commented 3 years ago

@Casteran can I do a language pass in the jfla2022 branch? And do you want all changes as pull requests, or should I just push minor fixes?

Casteran commented 3 years ago

Sure, please do ! The day after tomorrow I have a meeting with Théo in Bordeaux. May be the best is pushing the mandatory changes (typos, etc.) and sending PRs for the rest.

Le 21 sept. 2021 à 16:53, Karl Palmskog @.***> a écrit :

@Casteran https://github.com/Casteran can I do a language pass in the jfla2022 branch? And do you want all changes as pull requests, or should I just push minor fix?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/82#issuecomment-924067088, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQSROO6EVTA7QJAVI3UDCL53ANCNFSM5ELXOA4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

cpitclaudel commented 3 years ago

Hi folks! This sounds great, happy to be in. Please let me know what the best time for a meeting would be.

Casteran commented 3 years ago

Hi Clément !

Théo and I have a meeting on Friday. Could you compile the pdf ? If you notice something to add or correct, please send us mails or PR.

Best regards Pierre

Le 21 sept. 2021 à 17:26, Clément Pit-Claudel @.***> a écrit :

Hi folks! This sounds great, happy to be in. Please let me know what the best time for a meeting would be.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/82#issuecomment-924098920, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCXHAHX5DNULTAZGKULUDCP27ANCNFSM5ELXOA4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

Casteran commented 3 years ago

Le 21 sept. 2021 à 17:19, Castéran Pierre @.***> a écrit :

Sure, please do ! The day after tomorrow I have a meeting with Théo in Bordeaux. May be the best is pushing the mandatory changes (typos, etc.) and sending PRs for the rest.

Sorry : the meeting is on Friday, not Thursday!

Le 21 sept. 2021 à 16:53, Karl Palmskog @. @.>> a écrit :

@Casteran https://github.com/Casteran can I do a language pass in the jfla2022 branch? And do you want all changes as pull requests, or should I just push minor fix?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/82#issuecomment-924067088, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCQSROO6EVTA7QJAVI3UDCL53ANCNFSM5ELXOA4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

Zimmi48 commented 3 years ago

And tomorrow is Wednesday, not even Thursday. :laughing:

If you wish, we could do a video call with you all during my time in Bordeaux (I guess any time that works for you).

cpitclaudel commented 3 years ago

Théo and I have a meeting on Friday. Could you compile the pdf ?

Sure thing, I will do that!

If you wish, we could do a video call with you all during my time in Bordeaux

That would be lovely.

palmskog commented 3 years ago

@Zimmi48 a video call sounds nice. I think you can still see my general availability in the survey WG poll. I can stretch to 6pm or 7pm if that's the only slot that fits Clément.

Casteran commented 3 years ago

For me, any time until Friday 6h30 pm. Pierre

Le 21 sept. 2021 à 18:53, Théo Zimmermann @.***> a écrit :

And tomorrow is Wednesday, not even Thursday. If you wish, we could do a video call with you all during my time in Bordeaux (I guess any time that works for you).

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/82#issuecomment-924172408, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCR55ZFVDRJF232Q3ZDUDC2ABANCNFSM5ELXOA4Q. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

Zimmi48 commented 3 years ago

Let's say 4pm Paris time then. It should fit everyone's schedule if I'm not mistaken.

Casteran commented 3 years ago

I tried to explain better the relationship with the 2018 (in constant space!). The draft (not a PR yet) is on a branch small-changes.

cpitclaudel commented 2 years ago

I read through the text and opened a PR. Btw, I don't have a link for the call tomorrow. @Zimmi48 can you send it on Zulip?

coq-community / hydra-battles

Short paper on hydra-battles #82