Stream: Beginner Questions

Topic: Defining a function between function types

P Paturi (Apr 03 2023 at 11:57):

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).

Kevin Kappelmann (Apr 04 2023 at 06:34):

I am a bit lost what you want to do precisely. How would you define in mathematically? You can use Latex on Zulip
https://zulip.com/help/format-your-message-using-markdown#latex

P Paturi (Apr 04 2023 at 11:36):

I have a finite alphabet $A$ and the space of configurations $A^Z$, which are just functions $c:Z \rightarrow A$ (I am aware this could be done with bi-infinite lists, but I want to be able to generalize $Z$ to an arbitrary monoid later.) Let $r \in Z$. A shift map $\sigma_r: A^Z \rightarrow A^Z$ maps $c$ such that $\sigma_r (c) (x) = c (x+r)$, which is what I'm trying to define.

Manuel Eberl (Apr 04 2023 at 13:06):

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)"

P Paturi (Apr 20 2023 at 07:48):

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)

Simon Roßkopf (Apr 20 2023 at 08:26):

The types 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

P Paturi (Apr 20 2023 at 08:41):

Ah, I see. Thank you!

Last updated: Apr 27 2024 at 12:25 UTC