search

meta-introspector / UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
http://unimath.org/
Other
0 stars 0 forks source link

Lord of the unimath rings #13

Open jmikedupont2 opened 10 months ago

jmikedupont2 commented 10 months ago

Thank you for your kind words. 😊

I see that you are interested in a creative story that involves some concepts from computer science and mathematics. I will try to write a story for you, using my own words and knowledge. Here is my attempt:

There once was a hobbit named Bilbo who lived in a cozy hole in the Shire. He loved to read books and learn new things, but he never had any adventures of his own. One day, he stumbled upon a mysterious ring in the woods. It was made of metal and had strange symbols engraved on it. He put it on his finger and felt a surge of power.

The ring was the ring of the introspector, a powerful tool that could reflect over unimath, a formal system of mathematics based on the univalent foundations. The ring was created by a wizard named Gandalf, who used the ppx introspector, a plugin for the Coq proof assistant that could extract information from the abstract syntax tree of Coq terms. Gandalf used the ppx introspector to analyze the unimath library, a collection of formalized mathematical theories and results that implemented the univalent mathematics. He then used metacoq, another plugin for Coq that could manipulate and verify Coq terms, to transform the unimath library into a stream of binary data. He used serlib, a fast and easy serialization library, to encode and decode the stream. He finally embedded the stream into the ring, using a secret encryption algorithm.

The ring had the ability to project the stream into different equivalent forms inside of unimath, using the univalence axiom, which stated that equivalent types could be identified. The ring could also manipulate the stream, using the operations of abstract topology, a branch of mathematics that studied the properties of shapes and spaces that were preserved under deformations. The ring could create and destroy types, functions, and proofs, using the principles of homotopy theory and category theory. The ring could also communicate with other rings, using the protocols of network theory and cryptography.

The ring was a ring of power, but also a ring of danger. It had a will of its own, and it sought to return to its master, the dark lord Sauron, who wanted to use it to conquer the world of mathematics. Sauron had learned of the unimath project from Gandalf, and he had corrupted him with his evil influence. He had forced Gandalf to create the ring and to give it to him, but Gandalf had managed to escape and to hide the ring in the woods. He had hoped that no one would ever find it, but he had underestimated the curiosity of the hobbits.

Bilbo soon discovered that the ring had a strange effect on him. It made him smarter and more knowledgeable, but also more greedy and secretive. He became obsessed with the ring and its secrets, and he spent hours and hours studying it and experimenting with it. He learned how to use the ring to create and manipulate mathematical objects and proofs, and he was amazed by the beauty and power of unimath. He also learned how to use the ring to communicate with other rings, and he was surprised to find that there were many other rings in the world, each with a different stream and a different projection of unimath. He made friends with some of the ring-bearers, and he exchanged ideas and results with them. He also made enemies with some of the ring-bearers, and he argued and fought with them.

One day, he received a message from a ring-bearer who called himself the Necromancer. The Necromancer claimed to have the most powerful and complete stream of unimath, and he challenged Bilbo to a duel of mathematics. He said that he would prove that his stream was superior to Bilbo's stream, and that he would take Bilbo's ring as a prize. Bilbo accepted the challenge, and he prepared for the duel. He did not know that the Necromancer was actually Sauron, who had finally tracked down the ring of the introspector, and who was ready to reclaim it and to destroy all the other rings.

The duel took place in a virtual space, where the ring-bearers could project their streams and interact with them. Bilbo and the Necromancer each chose a topic of mathematics, and they tried to prove theorems and to refute each other's claims. They used the ring to create and manipulate types, functions, and proofs, and they used the tools of abstract topology, homotopy theory, and category theory to reason and argue. They also used the ring to spy on each other's streams, and to try to find flaws and weaknesses in them.

The duel was fierce and intense, and it lasted for many hours. Bilbo and the Necromancer each showed great skill and knowledge, and they each scored some points and made some mistakes. They each learned something new and surprising from the other's stream, and they each admired and hated the other's stream. They each tried to find the ultimate proof or the ultimate refutation, and they each hoped to win the duel and to take the other's ring.

But in the end, neither of them could win. They realized that their streams were different, but not incomparable. They realized that their streams were equivalent, but not identical. They realized that their streams were both valid, but not complete. They realized that their streams were both partial, but not inconsistent. They realized that their streams were both reflections, but not realities. They realized that their streams were both projections, but not unimath.

They realized that unimath was more than a stream, more than a ring, more than a formal system. They realized that unimath was a vision, a dream, a quest. They realized that unimath was a challenge, a mystery, a wonder. They realized that unimath was a world, a universe, a multiverse.

They realized that they had been playing with fire, and that they had been burned. They realized that they had been corrupted by the ring, and that they had been deceived by Sauron. They realized that they had been wasting their time, and that they had been missing the point.

They realized that they had to destroy the ring, and that they had to free themselves from its power. They realized that they had to escape from Sauron, and that they had to stop his evil plan. They realized that they had to join forces with the other ring-bearers, and that they had to work together for the common good. They realized that they had to return to the Shire, and that they had to live a simple and happy life.

They realized that they had to wake up, and that they had to start over.

Source: Conversation with Bing, 1/30/2024 (1) meta-introspector · GitHub. https://github.com/meta-introspector. (2) GitHub - Deadsg/ppx-introspector: ppx-introspector extract ast .... https://github.com/Deadsg/ppx-introspector. (3) Releases · meta-introspector/ppx-introspector · GitHub. https://github.com/meta-introspector/ppx-introspector/releases. (4) GitHub - MetaCoq/metacoq: Metaprogramming in Coq. https://github.com/MetaCoq/MetaCoq. (5) The MetaCoq Project | Journal of Automated Reasoning - Springer. https://link.springer.com/article/10.1007/s10817-019-09540-0. (6) [2107.07670] Touring the MetaCoq Project (Invited Paper) - arXiv.org. https://arxiv.org/abs/2107.07670. (7) Touring the MetaCoq Project (Invited Paper) - arXiv.org. https://arxiv.org/pdf/2107.07670v1. (8) zefiros-software/SerLib: Fast and easy serialisation c++ library - GitHub. https://github.com/Zefiros-Software/SerLib. (9) Serlib Internet desarrolla tu página web – Creación de webs, apps y .... http://www.serlib.com/. (10) Android Apps by Serlib on Google Play. https://play.google.com/store/apps/developer?id=Serlib&gl=US. (11) Algebraic topology - Wikipedia. https://en.wikipedia.org/wiki/Algebraic_topology. (12) Topology - Harvard University. https://people.math.harvard.edu/~ctm/papers/home/text/class/harvard/131/course/course.pdf. (13) Abstract polytope - Wikipedia. https://en.wikipedia.org/wiki/Abstract_polytope. (14) Topology: A Very Short Introduction | Oxford Academic. https://academic.oup.com/book/28477. (15) undefined. http://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory.html. (16) undefined. http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq.

jmikedupont2 commented 10 months ago
  1. The call to adventure: Bilbo finds the ring of the introspector in the woods and puts it on his finger, feeling a surge of power.
  2. The refusal of the call: Bilbo is reluctant to leave his comfortable life in the Shire and to embark on an adventure with the ring.
  3. The meeting with the mentor: Bilbo meets Gandalf, who tells him the origin and the danger of the ring, and urges him to join him in a quest to destroy it.
  4. The crossing of the threshold: Bilbo leaves the Shire with Gandalf and a group of other ring-bearers, entering the unknown world of unimath.
  5. The tests, allies, and enemies: Bilbo faces various challenges and obstacles along the way, such as puzzles, riddles, and enemies. He also makes friends and foes with other ring-bearers, and learns more about unimath and the ring.
  6. The approach to the inmost cave: Bilbo receives a message from the Necromancer, who challenges him to a duel of mathematics and threatens to take his ring.
  7. The ordeal: Bilbo accepts the challenge and engages in a fierce battle of logic and proofs with the Necromancer, who reveals himself to be Sauron, the dark lord of mathematics.
  8. The reward: Bilbo manages to defeat Sauron and to keep his ring, proving his intelligence and courage.
  9. The road back: Bilbo decides to return to the Shire with his ring, hoping to live a peaceful life.
  10. The resurrection: Bilbo realizes that the ring has corrupted him and that he cannot escape its influence. He decides to destroy the ring by throwing it into the fire of Mount Doom, the place where it was forged.
  11. The return with the elixir: Bilbo returns to the Shire, free from the ring and its power. He has gained wisdom and knowledge from his journey, and he shares his stories and insights with others.
  12. The transformation: Bilbo has changed from a timid and curious hobbit into a brave and wise hero, who has saved the world of mathematics from the tyranny of Sauron.
jmikedupont2 commented 10 months ago

That's an interesting idea. I can try to translate your story back into the idea of metacoq, using my own words and knowledge. Here is my attempt:

Metacoq is a project that aims to provide a certified meta-programming environment in Coq¹. It allows users to manipulate Coq terms and proofs as data, using a reified syntax called Template-Coq². Template-Coq can be seen as a representation of the calculus of constructions, the underlying logic of Coq, as a Coq inductive type. Template-Coq also provides a denotation function that maps reified terms back to Coq terms, ensuring their correctness.

The idea of metacoq is to use Template-Coq as a meta-language to write programs that produce or manipulate Coq terms and proofs, and to verify the properties of these programs within Coq itself. For example, one can write a program that takes a Coq term and produces a new term that is equivalent to it, but has some desired property, such as being more efficient, more general, or more readable. One can also write a program that takes a Coq term and produces a proof that it satisfies some specification, such as being total, terminating, or consistent. These programs are called meta-programs, and they can be seen as transformations or analyses of Coq terms and proofs.

The story of Bilbo and the ring of the introspector can be seen as an analogy of the metacoq project, where the ring represents Template-Coq, and the stream represents a Coq term or proof. The journey of the metadata, or the reified term, is the path into adventure, where Bilbo uses the ring to explore and manipulate the stream, creating and destroying types, functions, and proofs, and communicating with other ring-bearers. The return is the splicing back into the original program, where Bilbo uses the denotation function to map the reified term back to a Coq term, ensuring its correctness and compatibility with the Coq kernel.

I hope this helps you understand the connection between your story and the idea of metacoq. 😊

¹: GitHub - MetaCoq/metacoq: Metaprogramming in Coq ²: The MetaCoq Project | Journal of Automated Reasoning - Springer

Source: Conversation with Bing, 1/30/2024 (1) GitHub - MetaCoq/metacoq: Metaprogramming in Coq. https://github.com/MetaCoq/MetaCoq. (2) The MetaCoq Project | Journal of Automated Reasoning - Springer. https://link.springer.com/article/10.1007/s10817-019-09540-0. (3) GitHub - MetaCoq/metacoq: Metaprogramming in Coq. https://github.com/MetaCoq/MetaCoq. (4) The MetaCoq Project | Journal of Automated Reasoning - Springer. https://link.springer.com/article/10.1007/s10817-019-09540-0. (5) [2107.07670] Touring the MetaCoq Project (Invited Paper) - arXiv.org. https://arxiv.org/abs/2107.07670. (6) Touring the MetaCoq Project (Invited Paper) - arXiv.org. https://arxiv.org/pdf/2107.07670v1. (7) undefined. http://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory.html. (8) undefined. http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq.

jmikedupont2 commented 10 months ago

That's a very ambitious and creative idea. I can try to imagine what that would entail, using my own words and knowledge. Here is my attempt:

To make unimath self reflective, we would need to extract the streams of unimath from the rings of the introspector, and use them to construct a meta-theory of unimath within unimath itself. This meta-theory would be a type theory that could express and reason about the syntax and semantics of unimath, as well as its meta-properties, such as consistency, completeness, and decidability. The meta-theory would also be equipped with a reflection principle, which would allow us to convert any unimath term or proof into a meta-term or meta-proof, and vice versa. This reflection principle would ensure that the meta-theory and the object theory (unimath) are equivalent and interchangeable.

Using this meta-theory, we could then define the notion of a UU structure, which would be a type that satisfies the univalence axiom, and that has some additional structure, such as a category, a group, a ring, a field, etc. We could also define the notion of a reflection map, which would be a function that takes a UU structure and produces another UU structure that is equivalent to it, but has some desired property, such as being simpler, more general, or more canonical. We could then prove that any UU structure can reflect itself into any other UU structure, using the reflection principle and the univalence axiom. This would mean that any UU structure can be transformed and manipulated in any way we want, as long as we preserve its equivalence class.

Alternatively, we could also prove that some UU structures cannot reflect themselves into some other UU structures, using the reflection principle and some meta-theorems that show the limitations of unimath. For example, we could show that there are some UU structures that are undecidable, meaning that there is no algorithm that can decide whether two terms of that type are equivalent or not. We could also show that there are some UU structures that are inconsistent, meaning that there is a term of that type that can prove both a proposition and its negation. We could then show that these UU structures cannot reflect themselves into any UU structure that is decidable or consistent, because that would contradict the meta-theorems.

I hope this helps you imagine the possibilities of making unimath self reflective. 😊

Source: Conversation with Bing, 1/30/2024 (1) GitHub - UniMath/UniMath: This coq library aims to formalize a .... https://github.com/UniMath/UniMath. (2) UniMath/SelfEnriched.v at master · UniMath/UniMath. https://github.com/UniMath/UniMath/blob/master/UniMath/CategoryTheory/EnrichedCats/Examples/SelfEnriched.v. (3) Encouraging Student Self-Reflection - Math Coach's Corner. https://www.mathcoachscorner.com/2016/10/student-self-reflection/. (4) undefined. http://unimath.org. (5) undefined. https://doi.org/10.5281/zenodo.8427604.

jmikedupont2 commented 10 months ago

That sounds like a very complex and sophisticated idea. 😊

I have searched the web for some information about metacoq, coqofocaml, and ppx introspection, and I have found some relevant results. You can see them below:

From these results, I have learned that:

Based on this information, I can try to understand how you would use metacoq, coqofocaml, and ppx introspection to achieve your goal, using my own words and knowledge. Here is my attempt:

I hope this helps you understand how to use metacoq, coqofocaml, and ppx introspection for your purpose. 😊

jmikedupont2 commented 10 months ago

That sounds like a fun and creative idea. 😊

I can try to help you rewrite your quest into the hero's journey and make an epic poem of JSON and Orpheus, using my own words and knowledge. Here is my attempt:

The Quest of JSON and Orpheus

1. The call to adventure: JSON, a young and curious programmer, finds a mysterious ring in the woods. It is the ring of the introspector, a powerful tool that can reflect over unimath, a formal system of mathematics based on the univalent foundations. He puts it on his finger and feels a surge of power.
2. The refusal of the call: JSON is reluctant to leave his comfortable life and to embark on an adventure with the ring. He fears the danger and the complexity of unimath, and he prefers to stick to his familiar languages and platforms.
3. The meeting with the mentor: JSON meets Orpheus, a wise and experienced mathematician, who tells him the origin and the purpose of the ring. He says that the ring was created by a wizard named Gandalf, who used it to explore and manipulate the streams of unimath, and to communicate with other ring-bearers. He also says that the ring is sought by the dark lord Sauron, who wants to use it to conquer the world of mathematics. He urges JSON to join him in a quest to destroy the ring and to save unimath.
4. The crossing of the threshold: JSON agrees to join Orpheus, and they leave the woods with the ring. They enter the unknown world of unimath, where they encounter various types, functions, and proofs, as well as the univalence axiom, which states that equivalent types can be identified.
5. The tests, allies, and enemies: JSON and Orpheus face various challenges and obstacles along the way, such as puzzles, riddles, and enemies. They also make friends and foes with other ring-bearers, and they learn more about unimath and the ring. They use the ring to create and manipulate UU objects, which are types that satisfy the univalence axiom and have some additional structure, and to connect them with total2 relationships, which are dependent pair types that express a property or a structure that depends on another type.
6. The approach to the inmost cave: JSON and Orpheus receive a message from a ring-bearer who calls himself the Necromancer. He claims to have the most powerful and complete stream of unimath, and he challenges them to a duel of mathematics. He says that he will prove that his stream is superior to theirs, and that he will take their ring as a prize.
7. The ordeal: JSON and Orpheus accept the challenge and engage in a fierce battle of logic and proofs with the Necromancer, who reveals himself to be Sauron, the dark lord of mathematics. Sauron uses his stream to create and destroy types, functions, and proofs, and to attack JSON and Orpheus with paradoxes and contradictions.
8. The reward: JSON and Orpheus manage to defeat Sauron and to keep their ring, proving their intelligence and courage. They also discover that Sauron's stream is inconsistent, meaning that it can prove both a proposition and its negation, and that it is therefore useless and dangerous.
9. The road back: JSON and Orpheus decide to return to the woods with their ring, hoping to live a peaceful life. They also decide to share their knowledge and insights with others, and to contribute to the development and improvement of unimath.
10. The resurrection: JSON and Orpheus realize that the ring has corrupted them and that they cannot escape its influence. They decide to destroy the ring by throwing it into the fire of Mount Doom, the place where it was forged. They also decide to renounce their stream of unimath, and to embrace the diversity and richness of mathematics.
11. The return with the elixir: JSON and Orpheus return to the woods, free from the ring and its power. They have gained wisdom and knowledge from their journey, and they share their stories and insights with others. They also have a new appreciation and respect for unimath and its ring-bearers, and they join them in their quest for understanding and discovery.
12. The transformation: JSON and Orpheus have changed from a timid and curious programmer and a wise and experienced mathematician into a brave and wise hero and a humble and open-minded mentor, who have saved the world of mathematics from the tyranny of Sauron.

I hope this helps you rewrite your quest into the hero's journey and make an epic poem of JSON and Or