From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Authentication-Results: plum.tunbury.org; dkim=pass (1024-bit key; unprotected) header.d=inria.fr header.i=@inria.fr header.a=rsa-sha256 header.s=dc header.b=ECDQNNwN; dkim=pass (2048-bit key; unprotected) header.d=okmij.org header.i=@okmij.org header.a=rsa-sha256 header.s=pair-202411190653 header.b=T5aQfi+T; dkim-atps=neutral Received-SPF: Pass (mailfrom) identity=mailfrom; client-ip=192.134.164.83; helo=mail2-relais-roc.national.inria.fr; envelope-from=caml-list-owner@inria.fr; receiver=tunbury.org Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by plum.tunbury.org (Postfix) with ESMTP id D727A4AAAA for ; Fri, 13 Dec 2024 13:59:14 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=inria.fr; s=dc; h=date:from:to:cc:message-id:mime-version:in-reply-to: subject:reply-to:sender:list-id:list-help:list-subscribe: list-unsubscribe:list-post:list-owner:list-archive; bh=m0+Q9ghZgx8FvPwrG6TYK62U2B1HWfWL+HrsZSvWZyg=; b=ECDQNNwNbO89AfPRzf1rHu8U3mc4AJxiUmqCkoLKVMG7kwPLO7zBYw5V 2j4+Mc1Usc/hZQw7UD0q9Jn7+0z1Pvk1ygzIYH2kwyyL/wUyZxPmpcG/H Ztc2vANDABtp5dTLx4CuOywEVXNOAJdDHLALMEgbTmt05BgJWF57PQ8Xt w=; Received-SPF: Pass (mail2-relais-roc.national.inria.fr: domain of caml-list-owner@inria.fr designates 128.93.162.160 as permitted sender) identity=mailfrom; client-ip=128.93.162.160; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="caml-list-owner@inria.fr"; x-conformance=spf_only; x-record-type="v=spf1"; x-record-text="v=spf1 include:mailout.safebrands.com a:basic-mail.safebrands.com a:basic-mail01.safebrands.com a:basic-mail02.safebrands.com ip4:128.93.142.0/24 ip4:192.134.164.0/24 ip4:128.93.162.160 ip4:128.93.162.3 ip4:128.93.162.88 ip4:89.107.174.7 mx ~all" Received-SPF: None (mail2-relais-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@sympa.inria.fr) identity=helo; client-ip=128.93.162.160; receiver=mail2-relais-roc.national.inria.fr; envelope-from="caml-list-owner@inria.fr"; x-sender="postmaster@sympa.inria.fr"; x-conformance=spf_only Authentication-Results: mail2-relais-roc.national.inria.fr; spf=Pass smtp.mailfrom=caml-list-owner@inria.fr; spf=None smtp.helo=postmaster@sympa.inria.fr; dkim=pass (signature verified) header.i=@okmij.org X-IronPort-AV: E=Sophos;i="6.12,231,1728943200"; d="scan'208";a="199062308" Received: from prod-listesu18.inria.fr (HELO sympa.inria.fr) ([128.93.162.160]) by mail2-relais-roc.national.inria.fr with ESMTP; 13 Dec 2024 14:59:13 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id B302CE0D3F; Fri, 13 Dec 2024 14:59:12 +0100 (CET) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 4A4CEE0077 for ; Fri, 13 Dec 2024 14:59:06 +0100 (CET) IronPort-SDR: 675c3da9_15cXkPU/KUzpN+X5U7oIG5fk0PXiXifDFZMFmO+enzxoYJJ e6cOeYa5197Meho4Ck8JBoRBxgvGJyU3jd7Kvjg== X-IPAS-Result: =?us-ascii?q?A0EgBADQPFxndnIDJ0JagQmEF31aMwcISIglhS2IdWmfL?= =?us-ascii?q?Q8BAwENOQkCBAEBAwEDhQACimwCHwYBBDQTAQIEAQEBAQMCAwEBAQEBARABA?= =?us-ascii?q?QUBAQECAQECBAYBAhABPgNLhXsNgls7ghYsMFsBAQECAToGAQE3AQQWVkaDG?= =?us-ascii?q?4JBIwIBEQawSYE0gQGCDAEBBoEI3HsJgUiFa4JjAYloeicODYFIRYEVgjpwP?= =?us-ascii?q?oJKDAsDgiyFd4InhnmdHlJ7HANZIREBVRMXCwcFYUggKwOBFYIFgVsFN0eCS?= =?us-ascii?q?WlJOgINAjaCJHyCTYUZhGWEVYYdghmBawMDCx1AAwttPTcUG50PR4NZgT8Bg?= =?us-ascii?q?UamOaBKPIQkgW+CEIgZlUczhVuBSqMsmHuJfIQGmyiBfiOBXE0wCDuCZwlGA?= =?us-ascii?q?xkPly+8czQ1PAIHCwEBAwmFRYpdgUsBAQ?= IronPort-PHdr: A9a23:ZZnkixQbQ7Bi1o8cGzOA9TGuZ9psojyUAWYlg6HPa5pwe6iut67vI FbYra00ygOSBMOLtLkZ1aKW6/mmBTdYp87Z8TgrS99laVwssYYso0QYGsmLCEn2frbBThcRO 4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVImbuv6FZTPgMupyuu854PcYxlShDq6fLh+M Ai6oR/eu8QYnIduMKU8xxnGrnZIeuld2GdkKU6Okxrm6cq98oJv/z5Mt/498sJLTLn3cbk/Q bFEAzsqNHw46tfsuRffUwWE+2ESUn8RkhpGAgjF6A/1U5LsuSbkteRzxTeXM9TuQb87RTqt4 aFrSAT1iCgcLD427HvXis1rg61Fph+qugFyzJTVYIGRM/p+Y7/dcNYHTmdPQspdSypMCZ66Y oASDeQOIPxYopHzqVUOsxWzGxSiCuDgxTBUm3D537Y30/g9HQzcwAAsA84CvGrSod7oNKkSS +e1zKzQwDvaa/NZxzj945XPfxAmpfGDQ71wfNHWyUksEgPFj1eQpZbiPzOP2eQAqm6W5PdvW uyzkWAosR1xoiSxycc2jInEnpwZx07Z+Ch4wYs4K9O1RkB5bNCkDZZdqz+WOo9oT84+TGxlu Tg2xLIItJO/YiQG1Ikryh7dZvKHbYSF/h3tWPuXLDxlinxlf7e/iAyz8Uim0uD8Ucq00FNLr ipHiNXMsWoN1xPV58OaSfV95l+s1DeO2gzJ5OxJJVo4mKTBJ5I837I9mYIfvVnNEyL4gkn6k a+be0E+9uS15OnqZq/qqoGYOoJylwrzLKAumtGkAeQkLAcORXWV+eW91bL95UD1XLNHheAsn KbDqpDVP8Ebq7a5AwBL1oYj7A6yDzK839QZmXkLMUhJeB2JgoTzI1HBOvH4De2lj1uwlzdrw ujKPrznAprTMnjOiLbscLdn50NSzAc/195S64hJBr0cL///Qkrxu8bZDh89PQy02eHnCNBl2 4MZXWKAHKCZPbjVsV+L4+IvIuuMaJUSuDbnJPgp//jugmQhll8HYaapxYcXaGy/Hvl+PkmVe WDsjcsZEWcWogo+S/Tnh0GYXj5WY3a+RqY85jAgCIK6ForDXYCsgLmZ3CihBJFWZ2ZGCkqNE XjybYmEVe0MO2quJZpnkzcDUbG6DYE73Belsw7h47R9I+eS9DdLm4jk0Y1S4+Dc3UU18TF7J 8Oe1mCPCWZukTVbFHcNwKljrBklmR+42q9ijqkAfTQyz/ZAUwNgcIXZ0/Q/Edf5HATIYtaOT l+iBNSgGzA4CNwrkJcVe0goPdKkg1jY2jayRacPnumMAJE72qXf2nnzYcFnxCWOz7Ev2mEvW dAHLmi6nuh6/gnXCZTOlhCek6ulXaMf2S/PsmCZwjnGp1lWBTZ5Sr6NRnUDfg3WoND+s1vFV KOrAK87PxFpzMeDLvIMZYavlVxHXrHoP9G2j3uZvWC2CF7Iw7qNaNCvYGABxGDHD0NClQkP/ HGAPAx4ByG7omuYAiY8XVToK1jh9+VzshbZBgc90h2KYkt91rG05g9dhPqSTOkW164FvyFpo it9HVK01dbbQ9SaoA8pcKJZaNI7qFBJsACR/wt5M5OIKKNnh1xYdB54/gvv2xhxFoRcgJ0yt np5hAF2KK+ezBZAb2bGg9ara/uMbDCroEPKCeaewFzV3deI971a7f05rw+mpwS1Dg849H4h1 dBJ0nya75GMDQwIUJu3XFxkknoy77zcfCQ54JvZkHN2Nqzh+DjG1t0BA+ggyxTmeM1QevDMB ErpHssWCtL7YusulleBaREBPeIU87Q7dZDDFbPOyOugO+BumyijhGJM7dVm006CwCF7T/bBw 5cPx/zwMhKvbz7nlx/ht8n2ndoBfjQOBi+lziOiAodNZ6p0dIJNCGG0IsTxyM8sz5LqXndZ8 hakCTZkkIeufRedR1v+2AxSk0MNrjSrlDC5wDp9jzwy5vTBmnefhb+kLUNbcmdQDHFvl1LtP ZS5g5gBUU6kYhJo8XntrUf2yq5HpbhuemzaQENGZS/zfClpVqq9sKbHYtYats1u6nQRC6LlO AzJL9y16wEX2C7iAWZEkTUydjXw/478gwQ/kmWWanB6sHvef8h0gxbZ/t3VA/BLjV9kDGF1j yfaAl+kMpyn59KRwt3Etu2xf2WiU5xRNy7xwsnT/Dv+/mBsDRClyrq0ntDoOQ851C75kd5wW m+byXS0Kpmu3KO8P+V9e0BuD1Kp8Mt2FLZ1lY4ojY0R03wX1d2FuGAKmmDpPZBHyLrzOTATE CUTzYefs22HkAVza2iEzIXjWjCBz9t9MpOkN3gO1Ht15pJNC6KV7vpclCpvuVeisw/LJ/N6m 1J/gbMnunkZhuAL/g8kzyHbGrkTB1JVJzLhjVKD6NX2raNcYHujfOqq2U53jJa5BbCY5ApbX RObMt8jGyR088lyYk3B2nj664WiYNDRd5QYsRjc1h7Ei6I9xIsZrvMRnmInPGv8uSdg0Osnl Vl02pr8uoGbKmJr9ab/AxhCNzSzadlBsj3qiK9fmI6R0eXNVt15HS4XWZLzUf+yODcbtPC+c QnVViU1q23dEr3aVQOS80ZpqXvTHovjaS/RfyhflpM7HUXVLVc64khcRDggm58lCg2mjNfsd kt0/HFZ51L1rAdN1vM9NxT7VTSXrwOpZzEoDZmHeUQIqFoToRyTaJXCvYcRV2lC85asrRKAM DmebgVMVyQSX1CcQkrkNf+o7MXB9O6RAqy/KeHPaPOAs787Nb/AyJSx349h5zvJON+IOywoC Pk21WJEXnV4GYLegTpFGEl132rdKtWWohux4Hg9tsek7PHiQx7i/6OKArpWaJNgoFauiKaZc eWXgWwqTFQQnoNJznjOxr8F2VcUgCw7bDihH4MLsivVRb7RkKtaXFYLLjl+P8xS4+cgzxFAb ITF38jt2Ocy3ZtXQx9VEEbskcazaYkWLnGhYRnZUV2TOu3OLHWOysXzK8tUqJVVheRQ7lu/4 nCDGk75eD+EkmuwP/hKGeZPiSCZehtEt9PlGv6CIW/gSdPkLBqhP40u5QA= IronPort-Data: A9a23:95jH1qCTwN+42xVW/+jnw5YqxClBgxIJ4kV8jS/XYbTApDkhgzAEz 2ofXGqGM/eMY2f1L41zPYW0pB8OsJPTn9djOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yM6j8lkf5KkYMbcICd9WAR4fykojBNnioYRj5Vh6TSDK1rlV eja/YuGYjdJ5xYuajhIsvja80s21BjPkGpwUmIWNagjUGD2zCF94KI3fcmZM3b+S49IKe+2L 86rIGaRows1Vz90Yj+Uuu6Tnn8iGtY+DiDS4pZiYJVOtzAZzsAEPgnXA9JHAatfo23hc9mcU 7yhv7ToIesiFvWkdOjwz3C0usyxVEFL0OavHJSxjSCc51fDYUfl58ttNWsNMs5b0McuGT5A/ PNNfVjhbjjb7w636LeyS+01wMt4atHiPZlZsXZlpd3bJah4B8uSBf6MvIYEtNszrpgm8fL2Y M4UZhJobxHBYVtIIFh/5JcWxbb53ielKWEDwL6TjY5qwEft1VBS7IboLuHUftiVFMoKhFnN8 woq+EylXkpLbID3JSC+2nmlg+uKmSLgRKoJBbig/7hrhkeSzyodEnUruUCTpPC4jhf4VIkZM 0UV4Gwlqq1aGFGXosfVRRiqnHeggB0lceFfUK4QyViVlaTd7FPMboQbdQJpZNsjvc4wYDUl0 F6Vgt/kbQCDVpXIExpxEZ/J9luP1TgpEIMUWcMToeI4DzTLpYgyikuJQY0lCKe0lJv+HjSYL 9G2QMoW2eV7YS0jjvrTEbX7b9SE/MehoukdvFS/Y45dxlklDLNJnqTxgbQh0d5OLZyCUn6Kt 2Uels6V4YgmVM7WyHTXEL9cQOj5uZ5p1QEwZ3YyRPHNEBzwpxaekXx4vWomeS+Fz+5dJ2S5P Be7Vf15vcIDZBNGkpObk6rtV597lfSI+SXNTvnVdJJIb4RucxWE50lTib24gQjQfLwXufBvU b/CKJ7EJS9DWcxPkmDqL89DiuVD7n5lmgvuqWXTlkTPPUy2PS7NEe9t3ZrnRrxR0Z5oVy2Oq IcOZ5fWl083vS+XSnC/zLP/5GsidRATba0aYeQOHgJaCls4RjMSGLXKzKk/eodoua1Qm62at ju+Q0JUgh63z3HONQzAODgpZaLNTKRPiysxHRUtGlK0hFklQ4Kkt5kEe7UNILIIye1EzNxPd ccjRfmuOPp1d2n4y2wvVqWl9I1GXza3tD2KJBugMWQefYY/Zgnn+e3EXwrI9QsQB3DurcI// qOr0wjaZbEhRA1SKtncR9zy7lG2vFkbwPlTWWmRKPZtWUzcyqpYAA2vse0WeuYicQ7iwBme3 CaoWSYon/HH+dIJwYOYlJK6oJeMOMogOEhjRk3wz6u8bAve9Uqdmb5wav6CJ23hZTml6ZeZR Ltnyt/nO6c6h3dMiY13FohrwY8Y59fCo7x7zBxuLE7UbmaEW69RHX2b4fZh7qF95KdVmQ+Ta HK9/tN3PbaoOsS8NHUzIAEjTPqI1NBKuz30wMk2Hn7H535MzOLaaXlRAhiCszwCDb1XNIh+/ /wtlvRL4COCiz0rEO28sAZqy0q2IEctaZ4X7qMhPNeziy4A6E1zXpjHOyqnvLCNc4ptN2cpE B+1hY3DpapVnBPaentuC3PI1ut5rrYNsSBs01UtCQmomN3Ep/lvxzxX0209YTp0xyV98dBYG zZUJWwsAovW5BZupsxIf170KjF7HBfDp3DAkQoYplPWX2yDdzLrLlRkHc2v4UpA0WZXXgYDz YGi0Gy/DArbJpDg7BATB3xghefoF+Fq1wv4n8uiIcSJMr86bRfhgY6sfWA4kATmM+xgmHz4o fRWw8goZZ3ZLSIwp4gJO7ue35kUSzGGIzVmatNl96UrA2rdWW+T3R6jFkOPQf5Odsf6qRKAN 89TJ8x0R0uf0gSKpWslHqIiGeJ/s8Mow9sgQYnVA1A6nYGRlRdXla7B1zPfgTYrSup+kMxmJ YL2cSmDI1OqhnBVujHsqZBEM1Wncf0Bbx/Y2sq1+dUoCqNZ4f1NcF4z4JSwrX66IAtqxDPKn QLhNov97f1u9pRopKToSp58PgSTLcjhccix6yWxjoh+VszOOsLwqA8lkFnrEABIN783Wd4st 7CynPPo/UHC5pAabnv4nsSfKqx3+smCZupbHcbpJn18nyHZesvN4QMGyl+oO65yj9JRycm2d TSWMPLqW4YuZO5c43lJZwx1MRUXUf33Z5i9gxKNla2HDxxF3DHXKN+iy2TSUlhaUS01ILz7N B7/vqe/x9JfrbkUPiQ+OdNdP8ZaLmPgCIwcTP+ghQnAWyPsyhmHt6D5nBUt1SDTBzPWWIzm6 JbCXV7leA70pKjMy8pDvpdvugEMSkxwmvQ0YllX7useZ+pW14LaBb913VQ65pBofuja0Zj5Y GiLYzBkESz8R3JPdhCUDBHLQFKEHuJXUjvmDmVBwq9WQ37e6EC87H9J8SRl4nUwfSHspA1iA c9L4WX+Z3Bd3bkwLdv+JZWHbSNPwfDfx3BO/lry+yA379DyHp1SvEFc8MFxueAr3i0DeIgn5 YT4eIycfHyGdA== IronPort-HdrOrdr: A9a23:qBxxWarbENy7fzga9EEHWVUaV5oGeYIsimQD101hICG9E/b4qy nApoV56faZslwssRIb9+xoWpPtfZq0z/ccirX5VY3DYOCMggSVxe9ZgLcLCVXbak/DHi0079 YET0AFYueAamST1qzBkW+F+5JK+qj9zEhs7d2uq0uEiWlRGthdB8AQMHfiLnFL X-Talos-CUID: =?us-ascii?q?9a23=3Am0sL8WpvY0hQ6He+p8/sidXmUdogYEHU6EnTGmW?= =?us-ascii?q?DBiUqYpzMUQCe8awxxg=3D=3D?= X-Talos-MUID: 9a23:xsXVgwr6tupYVv9z+poezxU/F+hW+viNNH4Ij64Hv82bZCMvISjI2Q== X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="6.12,231,1728943200"; d="scan'208";a="199062243" X-MGA-submission: =?us-ascii?q?MDEIMDyHgky3Cugyyufaki7I1bhGlQzGif1TBw?= =?us-ascii?q?YS+wfORehCCvdv4wBx5vP7yDrHDKRVnoeSpy35MMlkwkARG2cl/VTG3v?= =?us-ascii?q?YrdGuHKnn1AxuvKIdxtk5PT2bAJvMteGYjVZl4UclIYMHrGqulFyYMLL?= =?us-ascii?q?P07kfohApZwb9E3E8jkuOZ9w=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 13 Dec 2024 14:59:04 +0100 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id E243A3FBAEA; Fri, 13 Dec 2024 08:59:01 -0500 (EST) Received: from Magus.localnet (29.149.159.133.rev.vmobile.jp [133.159.149.29]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id AAECD582E18; Fri, 13 Dec 2024 08:59:00 -0500 (EST) Date: Fri, 13 Dec 2024 22:58:23 +0900 From: Oleg To: nicolas.francois@free.fr Cc: caml-list@inria.fr Message-ID: Mail-Followup-To: Oleg , nicolas.francois@free.fr, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20241112230312.6fcf76ab.nicolas.francois@free.fr> DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=okmij.org; h=date:from:to:cc:subject:message-id:mime-version:content-type:in-reply-to; s=pair-202411190653; bh=m0+Q9ghZgx8FvPwrG6TYK62U2B1HWfWL+HrsZSvWZyg=; b=T5aQfi+TKF4Uhmh+qvOh+p/SdXIiUibss5GhxcOF+57g5+fz+VHwup7ZdiAC1fZpvvszb2IbMGG7PExgCvkvYdEhzfy0aGWpo+ugcEgWdZEL5KXq19kj5+cidj2PL7o0e0/um4D6sCnahEXDGJQkdmNjQHNu0vIMW3Rq7rE43m7bXpWnTFxYuPz9Kuux7mzTL86upbN0l6YsYP8jciQq53d3DuYFdrg81BebYbeFLwJ+ofIsFhuXehRSVRTxUeutjZpqANr4Z0GlhaUodcWxZFXpYZFHPpgJ2nuM7jK6f0RnattC8EowaI+YKO7GFfP1o6b174MKOyKAFiha4cuUZQ== X-Scanned-By: mailmunge 3.11 on 66.39.3.114 Subject: Re: [Caml-list] Problem formalizing a representation Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 19230 Errors-To: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Help: List-Subscribe: List-Unsubscribe: List-Post: List-Owner: List-Archive: Archived-At: > I'd like to represent logical formulas for different logics. > > A logic is syntactically represented by atoms, and rules involving (at > the very least) and, or, not, and possibly implies and equivalence... > > What differs between my logics is the atoms : > - for propositional logic LP, atoms are just variables, and > interpretations assign true or false to those variables ; You have probably received lots of help already. Just in case, let me mention that back in 2019 I gave a short course at a Dagstuhl summer school on meta-programming on a similar topic. It was formulated a bit differently: wires (instead of atoms) and logical gates (as connectives). http://okmij.org/ftp/tagless-final/course2/index.html Starting from zero, the course dealt with various transformations (NAND conversion), constant propagation (or unit propagation, as sometimes called) and finally the CNF conversion (normalization). Actually the course finished with circuits (gate assemblies with several inputs and outputs), full adder and applying unit propagation/CNF to all these things, but you probably don't need that. There was an exercise to make wires more interesting, like 32-bit busses. As you can see from the course materials, I talked a lot about parameterization.