Content deleted Content added
Line 375:
:::::: By mathematics I loosely mean ZFC based stuff. My only problem is saying that the Y combinator gives a solution of the fixed point equation. But then the fixed point equation is expressed in "mathematics", not LC. Anyway for me a value is a property of an expression (wff) that is the same iff the two expressions are equal. And a solution is a value that satisfies the equation. But maybe this not the standard definition for mathematician (only for other humans). My objection before was you referring to Y f as a solution of x = f x. I will re-read what you wrote in light of this discussion later. Regards [[User:Thepigdog|Thepigdog]] ([[User talk:Thepigdog|talk]]) 02:22, 15 January 2014 (UTC)
::::::: I think an intuitive (informal) notion of "value" that might work for you is that lambda terms are their own values so long as "equals" is expanded to convertibility as per the usual axioms of LC. This is a bit like providing semantics for lambda calculus using a term algebra generated by the usual formation rules for lambda terms. A better notion of value is a Bohm tree, which makes explicit the value of a non-normalising term (it still has a value). [[User:Haklo|Haklo]] ([[User talk:Haklo|talk]]) 04:40, 15 January 2014 (UTC)
==Its not magic==
| |||