Content deleted Content added
Line 378:
::::::: 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)
:::::::: I think a Bohm tree is OK for me as a value for LC. As I understand it, a bohm tree allows you to access parts of the value (like a record where some fields are given but not others). Does that help you in giving me a value for x = not x? Regards [[User:Thepigdog|Thepigdog]] ([[User talk:Thepigdog|talk]]) 06:42, 15 January 2014 (UTC)
::::::::: I've revised the [[Bohm tree]] page, although I haven't put references in yet and the phrasing is awkward because I've tried to keep it non-mathematical (and so I didn't quote Barendregt). It may help giving "values" for terms that do not have normal forms, but I don't think you need it for the "not" example; I think the fixed point I gave for that earlier should serve? [[User:Haklo|Haklo]] ([[User talk:Haklo|talk]]) 12:45, 16 January 2014 (UTC)
==Its not magic==
| |||