Minimal Logic For Dialectica Interpretation

[ last updated on 13 January 2021, first created on 20 May 2006. Copyright 2021 Hernest & Trifonov for differential changes relative to the original Minlog distribution ]

We here provide the full Minlog of August 2015 plus `etsmdA.scm', `mdiphVB.scm' and `initDan.scm' in the "minlog" root folder. The Scheme program extraction from a classical proof of Unbounded Pigeonhole Principle (UPP) by means of an implementation of Kreisel implication is presented in our paper. File mdiphVB.scm is for UPP, file etsmdA.scm adapts MinLog's native `pairs' Dialectica module etsd.scm by interpreting `-->' (impnc) as Kreisel implication, while initDan.scm is MinLog's `init.scm' for Windows pathnames. Simply replace "C:\\minlog" in the file minlog/initDan.scm with your actual minlogpath, like "~/minlog". Also replace "C:\\minlog\\initDan.scm" with `minlogpath/initDan.scm' and "C:\\minlog\\etsmdA.scm" with `minlogpath/etsmdA.scm' in the file minlog/mdiphVB.scm If you work under (any) version of Windows (hopefully XP Professional, or at least 7 Home Premium) and unzip in the root folder "C:\" then you are done.

In March 2008, the light (monotone) Dialectica with tuples was part of the main Minlog distribution (in parallel with the variant with pairs, developed and maintained by Schwichtenberg and Trifonov). At this moment the `diatup' module is no longer present in the latest MinLog distribution, due to (backwards) syntax compatibility. Nonetheless we here provide the half-MegaByte full MinLog of 2008. The extraction module is "modules/diatup.scm" and the examples are under "examples/diatup/*". The older development snapshots (previous to March 2008) are here. Check 080303 for the historically first `tuples' variant integrated with mainstream Minlog.

Installation Instructions

It is assumed that you have (Petite) Chez Scheme installed on your Computer. A very useful option, particularly when working with the Petite Interpreter is to also have Emacs installed on your Computer.

Each snapshots is a ZIP archive of the "minlog" folder and the relevant part of its contents. Simply replace "C:\\minlog" in the file minlog/init.scm with your actual minlogpath, like "~/minlog". Also replace "C:\\minlog\\init.scm" with `minlogpath/init.scm' in all example files. If you work under (any) version of Windows (hopefully XP Professional, or at least 7 Home Premium) and unzip in the root folder "C:\" then you are done. Enjoy!

Contact and Technical Support

Should you have any questions about Installation or about light and/or modal Dialectica interpretations, you are welcome to write us at danhernest@gmail.com or even better, at triffon@fmi.uni-sofia.bg