On Wed, Jan 20, 2021 at 08:06:45PM -0800, Stuart Hungerford wrote:
> On Thursday, 21 January 2021 at 10:22:45 UTC+11 Jens Axel Søgaard wrote:
>
> Den ons. 20. jan. 2021 kl. 08.43 skrev Stuart Hungerford <
> > stuart.h...@gmail.com>:
> >
> >> On Wednesday, 20 January 2021 at 12:34:59 UTC+11 Robby Findler wrote:
> >>
> >> I'm no expert on algebras, but I think the way to work on this is not to
> >>> think "what Racket constructs are close that I might coopt to express
> >>> what
> >>> I want?" but instead to think "what do I want my programs to look like"
> >>> and
> >>> then design the language from there, reusing libraries as they seem
> >>> helpful
> >>> or designing new ones that do what you want. Racket's
> >>> language-implementation facilities are pretty powerful (of course, if
> >>> there
> >>> is nothing like what you end up needing, there will still be actual
> >>> programming to do ;).
> >>>
> >>
> >> Thanks Robby -- that's a very interesting way to look at library design
> >> that seems to make particular sense in the Racket environment.
> >>
> >
> > An example of such an approach is racket-cas, a simple general purpose
> > cas, which
> > represents expressions as s-expression.
> >
> > The polynomial 4x^2 + 3 is represented as '(+ 3 (* 4 (expt x 2)))
> > internally.
> >
> > The expressions are manipulated through pattern matching. Instead of
> > using the standard `match`, I wanted my own version `math-match`.
> > The idea is that `math-match` introduces the following conventions in
> > patterns:
> >
>
> This is also fascinating (and very useful) -- thanks. This package
> illustrates the build-your-own-notation approach nicely.
> [...]
>
> > Back to your project - what is the goal of the project?
> > Making something like GAP perhaps?
> > Do you want your users to supply types - or do you want to go a more
> dynamic route?
>
> My project is really aimed at supporting self-directed learning of concepts
> from abstract algebra. I was taught many years ago that to really
> understand something to try implementing it in a high level language. That
> will soon expose any hidden assumptions or misunderstandings.
>
> An early attempt (in Rust) is at: https://gitlab.com/ornamentist/un-algebra
>
> By using the Rust trait system (and later Haskell typeclasses) I could
> create structure traits/typeclasses that don't clash with the builtin
> numeric types or with the larger more production oriented libraries in
> those languages in the same general area of math.
>
> Once I added generative testing of the structure axioms I could experiment
> with, e.g. finite fields and ensure all the relevant axioms and laws were
> (at least probabilistically) met.
>
> Thanks again Jens.
You might also want to look at the implementations of category theory in Agda.
Agda is a language which unifies execution and correctness proof to some
extent.
Not that you want to implement catagory theory, but category theory is a
form of algebra, and you may find some useful ideas about syntax and
semantics there.
I attended an online seminar about this recently, but I haven't been
able to find the details again. The following links seem to refer to the
same project. (I found them looking for
category theory in agda
on duckduckgo.
The software:
https://github.com/agda/agda-categories
Documents:
Formalizing Category Theory in Agda
pdf: https://arxiv.org/pdf/2005.07059.pdf
slides: https://hustmphrrr.github.io/asset/slides/cpp21.pdf
Agda itself is also worth a look.
As well as older proof assistants like coq.
There's definitely a trand towards constructivism in foundational
mathamatics.
-- hendrik
> Stu
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/b14e56eb-71ef-49f4-8e98-fea4ced6e3adn%40googlegroups.com.
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/20210121135543.qi2rth7qkhlasrcc%40topoi.pooq.com.
