New answers tagged lambda-calculus
2
The meaning of curry can be easier to be seen when the type signature is written as
curry :: ((a, b) -> c) -> (a -> b -> c)
that is, a function taking a single parameter of type (a, b) and yielding a result of type c is turned into a function taking two separate values of types a and b yielding the same result type c.
We might define curry for ...
3
$C$-monoids and their variants is what you are looking for. You can find further references and an account of what is what in Martin Hyland's Towards a Notion of Lambda Monoid.
4
Well nevermind this has an easy answer.
Let $r_n = \lambda x_1 ... x_n . \lambda p . p \: x_1 ... x_n$
Note that for $m < n$, $r_n\: A_1 ... A_m$ normalizes for any normal $A_1 ... A_m$.
Then for any $f$, let $n$ be larger than the number of subterms in $f$.
$f \:r_n$ normalizes, so therefore no $f$ exists which only normalizes for a specific input.
2
Here is a new paper that covers a similar topic. The idea is that by doing algebra in enriched categories (2-categories are like categories enriched in categories), you can talk about more fine grained semantic structure on the algebra. (I haven't read through the whole paper myself, but I know enough to see some of the ideas behind it.)
The way it relates ...
Top 50 recent answers are included
