coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Alex Shkotin <alex.shkotin AT gmail.com>
- To: coq-club AT inria.fr
- Cc: martin.dvorak AT matfyz.cz
- Subject: Re: [Coq-Club] Grammars
- Date: Thu, 25 Aug 2022 10:50:55 +0300
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=alex.shkotin AT gmail.com; spf=Pass smtp.mailfrom=alex.shkotin AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f51.google.com
- Ironport-data: A9a23:r9HM764Yn9pnLO32C2vVbQxRtBvBchMFZxGqfqrLsTDasY5as4F+v jAdCm+HbKqMYmLxLt9zOovn9kIO6pTTx9ZhQFE++yk9Zn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2eaEvfDjW1nX4 YOo/pWGULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 N5QmZObZFY4BbCSt6cWfCFcMQ9uF4QTrdcrIVDn2SCS50jPcn+p3e43SU9rZMsX/eF4BWwI/ vsdQNwPRkrb1qTmnfThE7Yq251LwMrDZOvzvllpyTzJS+0mQpffQqPi6tpR3TN2jcdLdRrbT 5ZIOGMxPEyRC/FJEn44Nqg8wcaWv1TUUSRKs3+Xl7stuUGGmWSd15C0aIaPEjCQfu1emV/dr Wbb9UziExQCPZqezyCE+zSinIfycTjTXYsTEPim7acvjgDKgGMUDxISWB2wpvzRZlOCt8x3I FE49QED/LkJ6RKEDdLSZxmajm6ul0tJMzZPKNES5AaIw6vSxg+WAGkYUzJMAODKUudmFVTGM XfZz7vU6SxTXK69Ei3Cq+/Fxd+mEW1Ecj9YPH5soR4tuoG7+OkOYgTzosGP+ZNZY/XwEDD0h i6R9W0w2uxVgskM2KG2u1vAhlpAR6QlrCZluW07vUr/tmuVgbJJgaT2sjA3Ct4edu6koqGp5 iRspiRnxLlm4WuxvCKMWv4RO7qi+uyINjbR6XY2Qcd4rGrwqyX5I9EOiN2bGKuPGpZUEdMOS B+D0T69GLcOVJdXRfQqPdzpWpRCIVbITIm+DKy8giVyjmhZLVfbpkmClGaf2GfilEVErE3ME cbzTCpYNl5DUf4P5GPuGY81iOZ3rghjmz67bc2kl3yPj+DCDFbLEuxtGAXVPogEAFas+lq9H yB3bJvUlX2ykYTWPkHqzGLkBQlbciRlW8mt9Zw/myzqClMOJVzNwsT5mdsJE7GJVYwM/gsR1 n3iCEJe1nTlgnjLdVeDZnx5OeHgWJ9+qTQwOil1ZQSk3H0qYICO6qYDdstvLeN3qrA7lfMkH eMYf8igA+hUTmuV9jkYa677ptMweRmugzWIICf4MiM0eIRtRlCS99K9Jlnv+SACAzCZr8w7p 7H8hArXTYBSFQtnBcfSLvmoygrp73QanetzWWrOI8VSKB28qtg0d3Spg6Zucc8WKBjFyj+L7 CqsAE8V9bvXvos40NjVnqTb/YqkFu1JGEAFTWTW6LCBMzaDojiuzIpGZ+a/fT7HUVTy9qj/N /5eyOvxMaFekVtH79h8HrJswf5s7tfjveUBnAFtHXGOcU/yT709ez+J2s5AsqALzbhc4FPkV kWK89hcGLOIJMK1TwJLdVR9NryOhaMOhz3fzfUpO0GmtiV5y7yKDBdJNB6WhS0BcbZ4bNE/z eE6tJJE4gCzkEBxYNOPjyQR6X/Va3JdCuMosZYVBIKtgQ0ukwkQbZvZAy7wwZeOd9QcbRVwc 2HM3PLP1+ZG207PU3svDnyRj+BTspID5UJRx1gYKlXVx9fIi5fbBvGKHejbk+iU8vlG7w63E m1iNkkwO77Xujk13Y5MWGejHwwHDxqckqA0J53li0WBJ3RElESURIH+BQpJ1E8c+mNYODNc+ dl0DU77BC3ycpiZMjQaACZYRj+KcTC13gLHkcGjWc+CGvHWpNYjbrCGPQI1lvcsPS/9aIAra wWnECacpJAX7RItnpA=
- Ironport-hdrordr: A9a23:ngd69ag8+6YTP6QIqDhsCib0k3BQXuUji2hC6mlwRA09TyVXrb HWoB17726NtN91YhsdcL+7Scy9qB/nhPxICMwqTNSftWrd2VdATrsSibcKqgeIc0bDH6xmtZ uIGJIOb+EYY2IK6/oSIzPVLz/j+rS6GWyT6ts2Bk0CcT1X
- Ironport-phdr: A9a23:71UxLR/N8G3Qxv9uWfG2ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Z wqFuq8m1QWTFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo5ZHeYRtEiDWgbb9sM hm9sBncuNQRjYZ+MKg61wHHomFPe+RYxGNoIUyckhPh7cqu/5Bt7jpdtes5+8FPTav1caI4T adFDDs9KGA6+NfrtRjYQgSR4HYXT3gbnQBJAwjB6xH6Q4vxvy7nvedzxCWWIcv7Rq0yVD+/7 alkVQXohT8IOD438m7ZisJ+gqFGrhy/uRFw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b 44XAucdOeZXsYb8rEYToxu+BgmsA//vyj5OhnTr2qA1yeAhHh/J3QA6BNIOsHfUrNLpNKcTV +C416bIzTDZYPNX3Tfx8pTHchckofyVW797bMXex1U1GQzfklWQtZLqPymT1ukVsmWV4eRtW OOvhmM7tQx8vDiiy8kwhofGh48Yy1DJ+ytnzYorKtO2SFB3bcOqHZZetCyXNoV7T8wiTWxrp Cs21rsLsoO1cigNzZQo3R/fa/qffoiS/B3jT/ieLi1ihH15eLK/iAy98VS+xeHmUMm7zkpKo jJKktnNqnAN1wHT5dOdRvRh+Ueh3C6D1wHI6uFYO084j7DUJII7zrEqipoet1nIECzumEjuk qOaakEp9vKr5unneLnquIKQOo1uhgz+L6gjnNG0D/4iPQgURWeb/Pyx1L398k39R7VHlvg2n bPYsJDePMgbuLW5DxJM3oYt6xuzEi2q0NsfnXkAI1JFfAyIg5L1NFHJJfD0Ffa/g1Kynzd33 /3KIKHtD5HXInXAkLrtZ6hx51NexQYpzd1T+opYCrQbL/LyXk/xusbYDhg8MwGs2ennDMty1 4wEVWKUAq+ZM6TSsUOJ5uIpOOSMa4oVtyz8K/gh/fLhkXg5mVoFcamvxpQYcGq4Eeh+I0WFf Xrshc8MHXoSsgokUOPqkEGCUSJUZ3uqQ6084Sg7BJu6AofHW4Cim6eM3Dy7H51TfmBJEEqAE Xbud4WeWvcDcjieIsF7km9Mab/0QIg4kBqqqQXSyrx9L+OS9DdLm4jk0Y1c4+DD3Soy9jtoD sLVh2iJQnEyhWMLQCM32ohwpEV8zhGI1q0u0K8QLsBa+/4cClRyDpXb1eEvU7gaOyrEd9aNE hO9R8m+RCs2RZQ3ysMPZEB0H5OjiArC1mykGexdjKSFUboz9K+UxH3tP4Bl0X+T3a0snx89Q shIKWygrqF6/gnXQYXOlhbRjL6kIJwVxzWF72Kf1SyLtUBcXhR3VPDMWX0PIFDWrtPl50XqQ LqnCLBhOQxEmoaZMqUfTNrvgB1dQev7ftTTZ2Xkg2CrGROB3a+BdqLvcmQZmTvGUQ0KzllV8 nGBOgwzQCympgoyFRRIElTiKwPp+Oh68jagS1MsihuNZAtn3qa0/RgcgbqdTekS1/QKonVpr TI8B1u709/MbrjI7wN8YKVRZ88861ZbxCrYsQJ6JJmpM6FlgBYXbQ12u0rk0xg/BJ9HlIAmq 3YjzQw6Lqz9shsJfjeVzdbrOr7QNmj01B+qYq/SnFrZ1Zfe+6sC7ug5t0S2pBugRS9Auz1s1 9hY1WfZ542fVlJDF8KsFBxuqF4n/uK/AGF1/Y7f2HxyPLPhtzbD34hsH+450lO6eNwZNqqYF Qj0GslcBs60KeVslUL6C3BMdO1U6qMwONurMvWc36v+du9kkSLglmRE55x81GqD8iN9TqjD2 JNPkJT6lkOXEizxilusqJW9kIRJdXcJHmm41SniLIFUb6x2O40MDC39Rq//jsU7jJnrVXlC8 VelDF5Tw86ldy2ZaFnl1BFR30AayZC+sROx1Cc80zQgr67FmTfL3/ynbh0MfGhCWGhli17oZ 4myldETGkayPUAlkx6s5ECywKY+xuw3Jm3eUQFTfyvxM2BkeqS1v7uGJcVI7dskvD5WX+K1f V2BAuSl8l1KjmW5RjQYmWlzfiriopjjmh1mlG+RSRQ75GHUf81931aX5dDRQ+JQwitTQSB5j TfNAV3vd9Kt/NiSi9LCqrXkDzPnBsAVK3C0i97Z507ZrSVwDBaynu6+gIjiGAk+i2rg0sVyE D/Pp1D6a5Xq0KKzNaRmeFNpDRny8ZkfeMk2n40uiZUXwXVfiI+S+C9NmGP+IZNA2aH5cHsLb TEOyt/RpgPi3QcwSxDBj5K8TXibzsZ7MpOzZm4GnDk97MdWCaG847lNnC8zqV2951G0A7A1j nIWzv0g72QfiucCtV82zymTNbsVGFFRIS3mkxnbp8D7tqhcY3yjNKShzEcr1870F6mM+0sPP RSxModnByJ76d9zdU7BwGGmoJ+xY8HeNJoSrkHGyEqG1rkNbshtybxSwnA7cWPl4S97l6hh1 kcohM/i+tDAcjQInurxAwYEZGOrIZpLoHe1y/4ZxJ7e3pjzTMs/XG9XDd24FbTwV2hK/fX/a 1TRSntl9jHCSOCZRUjGuCIE5zrOC8z5aC3RfSNEi40kHF7EegRemFxGBW1q2MdmSUb6gpSmK h4x5yhNtAen8V0Vm74ub1+nFT6BwWXgIjYsFMrFdEsQvlwEvh2Fd5TZt707HjkErMf48krQe irCNl4OVSZQCwSFHwyxZODwo4Oboq7DXKzmaKKfBNfG4fpXU/PCrX62+q1h+TvEdsCGP304S uY+xlIGR3dyXcLQhzQITSUT0SPLdc+S4hmmqGVxqYik/fLnVRiKh8PHAqZOMdhp5xG9gLuSf ++WiiFjLD9E15QKjXbWwbkb1VQWhmlgbT6oWbgHsCfMSurXlMo1R1YDbDhvMcJT868m9gxEO MqelMisk7Al17g6DFBKUVGnkcasJIQLL2y7KFLbFROLObCBdlipi4n8ZaKxT6EVjf0B7UXh/ 2bGVRW6YXLezmqMNVjnK+xHgSCFMQYLvYi8dkwoEm3/VJf8bRb9NtZrjDowyLlyh3XQNGdaP yIvFiEF5rCW8y5che1yXmJb6X8wZ+CAljbf9OnbLYoXt9NkBy11k6RR53FwmN43pGlUAed4n ifftIsku1a9juyG0SZqSjJLozdPwZyQ5ABsZPyf+Z5HVnLJuhkK6C/DbnZC78sgAdrptadKz 9HJn6+mMzZO/eXf+s4EDtTVIsaKWJLOGRXsET/QSgACSGzyXYk6r0NYmfCWsHaSq8piwnANs J8HS7seSkdsU/1HUwJqG9sNJJoxVTQhw+bzsQ==
- Ironport-sdr: 20/4HIwhS0WC2V334j0FtOLQYGdbQIi6Kf047juOW/AavH2T6X8iYYXOItkCxbQjX/tqhyNjxQ md+nrHCpzSbOp3+9pLBj7rXgToNqI0vxwql9gitltw/UO2xPfbLFR0hNCKPJ2KAPC+tqCndRR3 nuPjFOMR9DeD99Yvme0fRJrfzFizlDHVZNcq1bja1U0q0TpWdt6oyLKhGbNJcZssc6vARH1QSL hnYN9gZNHDNaJguZOEmtr9xB2BRylmnL98zwW8NKvwWrYnL0t8LEjSqlGArtzB1BgC2+XFXyNj gLRwqhEXoIw6uf89WtlcFpWD
Hi Martin!
Very interesting project! It looks like you are formalizing some Formal language theory. Which one? What textbook do you use?
Please have a look at [1] just for fun.
Best regards,
Alex Shkotin
чт, 25 авг. 2022 г. в 09:57, <martin.dvorak AT matfyz.cz>:
Dear Coq users,I work on formalization of formal grammars in Lean. I want to formalize the Chomsky hierarchy; the emphasis is on closure properties.Has anything similar been done in Coq? I have seen context-free grammars (the author had done much more than I did) but not general grammars yet.Best regards,
--
Martin Dvorak+436704091492All dates are written in the international (ISO 8601) format YYYY-MM-DD.All times are written in the Central European (Summer) Time (Vienna, Prague, Warsaw, Berlin, Paris, Madrid, Rome, …).
- [Coq-Club] Grammars, martin.dvorak, 08/25/2022
- Re: [Coq-Club] Grammars, Alex Shkotin, 08/25/2022
Archive powered by MHonArc 2.6.19+.