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 <
> > [email protected]>:
> >
> >> 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 [email protected].
> 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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/20210121135543.qi2rth7qkhlasrcc%40topoi.pooq.com.
