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

https://zulip.com/help/format-your-message-using-markdown#latex

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.

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)

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

Ah, I see. Thank you!

Last updated: Dec 07 2023 at 08:19 UTC