7 ms·

Can someone explain how is this different from lambda calculus, it seems like you can derive the same in both. I don't understand both well enough and hence the

by evnix 5mo ago

Can someone explain how is this different from lambda calculus, it seems like you can derive the same in both. I don't understand both well enough and hence the question.

bollu 5mo ago
Lambda calculus talks about computable functions, where the types of the inputs are typically something discrete, like `Bool` or `Nat`. Here, the domain is the real numbers.
TJSomething 5mo ago
The short answer is that the lambda calculus computes transformations on digital values while this is for building functions that can transform continuous (complex) values.
tromp 5mo ago
Any lambda term is equivalent to a combinatory term over a one-point basis (like λxλyλz. x z (y (λ_.z)) [1]). One difference is that lambda calculus doesn't distinguish between functions and numbers, and in this case no additional constant (like 1) is needed. [1] https://github.com/tromp/AIT/blob/master/ait/minbase.lam https://github.com/tromp/AIT/blob/master/ait/minbase.lam
sigmoid10 5mo ago
Lamda kind of does this in an analogous form, but does not allow you to derive this particular binary expression as a basis for elementary functions. There is a related concept with Iota [1], which allows you express every combinatoric SKI term and in turn every lambda definable function. But similar to this particular minimalist scientific function expression, it is mostly of interest for reductionist enthusiasts and not for any practical purpose. [1] https://en.wikipedia.org/wiki/Iota_and_Jot https://en.wikipedia.org/wiki/Iota_and_Jot
layer8 5mo ago
Lambda calculus is about discrete computations, this is about continuous functions. You can’t reason about continuous functions in lambda calculus.
- Twey 5mo ago
  Depending on your lambda calculus! From a categorical perspective a lambda calculus is just a nice syntax for Cartesian closed categories (or similar, e.g. *-autonomous categories for linear lambda calculus) so you can use it to reason about anything you can fit into that mould. For example, Paul Taylor likes to do exactly this: https://www.paultaylor.eu/ASD/analysis#lamcra https://www.paultaylor.eu/ASD/analysis#lamcra

by evnix 5mo ago

Can someone explain how is this different from lambda calculus, it seems like you can derive the same in both. I don't understand both well enough and hence the question.

bollu 5mo ago

Lambda calculus talks about computable functions, where the types of the inputs are typically something discrete, like `Bool` or `Nat`. Here, the domain is the real numbers.

TJSomething 5mo ago

The short answer is that the lambda calculus computes transformations on digital values while this is for building functions that can transform continuous (complex) values.

tromp 5mo ago

Any lambda term is equivalent to a combinatory term over a one-point basis (like λxλyλz. x z (y (λ_.z)) [1]). One difference is that lambda calculus doesn't distinguish between functions and numbers, and in this case no additional constant (like 1) is needed. [1] https://github.com/tromp/AIT/blob/master/ait/minbase.lam https://github.com/tromp/AIT/blob/master/ait/minbase.lam

sigmoid10 5mo ago

Lamda kind of does this in an analogous form, but does not allow you to derive this particular binary expression as a basis for elementary functions. There is a related concept with Iota [1], which allows you express every combinatoric SKI term and in turn every lambda definable function. But similar to this particular minimalist scientific function expression, it is mostly of interest for reductionist enthusiasts and not for any practical purpose. [1] https://en.wikipedia.org/wiki/Iota_and_Jot https://en.wikipedia.org/wiki/Iota_and_Jot

layer8 5mo ago

Lambda calculus is about discrete computations, this is about continuous functions. You can’t reason about continuous functions in lambda calculus.

Twey 5mo ago
Depending on your lambda calculus! From a categorical perspective a lambda calculus is just a nice syntax for Cartesian closed categories (or similar, e.g. *-autonomous categories for linear lambda calculus) so you can use it to reason about anything you can fit into that mould. For example, Paul Taylor likes to do exactly this: https://www.paultaylor.eu/ASD/analysis#lamcra https://www.paultaylor.eu/ASD/analysis#lamcra