Hello everyone! I'm trying to define a function between function types and I'm not sure what the correct syntax is. Generally, I want to map function f to function g such that the definition of g depends on f.
More specifically, I have a configuration c which is a function from a monoid (int for the sake of simplicity) to a finite alphabet, and want to define a shift map which maps it to another configuration e such that e(x) = c(x+r) where r is some shift constant.
I have defined the type synonym 'a config = "'a => alfa" (where alfa is the alphabet) and I am trying to define the shift as a function 'a config => => 'a => 'a config (where the second argument would be the shift constant).
I am a bit lost what you want to do precisely. How would you define in mathematically? You can use Latex on Zulip
I have a finite alphabet and the space of configurations , which are just functions (I am aware this could be done with bi-infinite lists, but I want to be able to generalize to an arbitrary monoid later.) Let . A shift map maps such that , which is what I'm trying to define.
What about this?
definition shift :: "int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a" where "shift r c x = c (x + r)"
Or, equivalently, this:
definition shift :: "int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a" where "shift r c = c ∘ ((+) r)"
This would not work for what I want, because what I want out is a function of type int => 'a, not just 'a. This is so I can for example create sets of shifted configurations. (If anyone has an alternative way of defining configurations on int in mind, that could also work)
int ⇒ (int ⇒ 'a) ⇒ int ⇒ 'a and
int ⇒ (int ⇒ 'a) ⇒ (int ⇒ 'a) are equal. So partially applying, like
shift r c should give you what you need
Ah, I see. Thank you!
Last updated: Dec 07 2023 at 08:19 UTC