Email Gateway (Aug 22 2022 at 19:26): Email Gateway (Aug 22 2022 at 19:26):From: Ken Kubota <mail@kenkubota.de>
For a natural expression of group theory type abstraction should be implemented, as suggested by Mike Gordon:
"[…] 'second order' λ-terms like λ𝛼. λx:𝛼. x, perhaps such terms should be included in the HOL logic." [Gordon, 2001, p. 22]
With type abstraction the mechanism of lambda notation can be used to _syntactically_ express the dependencies (here between the term and the type level), which follows the very idea of type theory.
See also:
http://owlofminerva.net/kubota/software-implementation-of-the-mathematical-logic-r0-available-for-download/
https://sourceforge.net/p/hol/mailman/message/35458077/ (section 5)
For a demonstration of an implementation (PDF) run
make group.r0.out.pdf && open -a Preview $_
make xor_group.r0.out.pdf && open -a Preview $_
For a demonstration of an implementation (HTML) run
make group.r0.out.html && open -a Safari $_
make xor_group.r0.out.html && open -a Safari $_
on a Mac after downloading the software (license restrictions apply) at
http://doi.org/10.4444/100.10.3
PDF generation requires Pandoc with LaTeX installed, and HTML view will cause a call to mathjax.org as the JavaScript display engine for mathematics.
Kind regards,
Ken Kubota
Ken Kubota
http://doi.org/10.4444/100
Last updated: May 06 2024 at 12:29 UTC