151:
22:
74:
53:
833:
8. "represents two values in the domain of the signed numbers. However it is a lambda expression so has only one value in the lambda calculus domain. Beta reduction of this lambda term never reaches normal form. However it represents a value, so a single value in the lambda calculus domain represents
512:
Since x was defined by the equation x = ¬x, it cannot be defined again as y y. So, apparently y shall be defined here as a (or: the only?) solution of the equation x = y y. In order for this definition to be acceptable, it should be justified why such a (unique?) solution exists. As a side remark, it
454:
I have modified the text in order to clarify the text. For point (1) I am trying to start with a computer programmers understanding of lambda
Calculus, where lambda calculus is as an expression in the domains commonly used in mathematics. In section 6 Domain of lambda calculus, I attempt to explain
471:
Thank you for your explanations. Unfortunatley, I still don't understand your argumentation. I have put some new lengthy "clarify" requests at some places where I have problems. Feel free to remove them if you find them annoying - I'm aware that they should better be discussed on this talk page, but
569:
But too many brackets are confusing for the reader (and me). I have added the let expression to the new terminology section. I hope that will suffice. Let and in bracket a condition, applied to another condition. I haven't specified exactly what the precedence is but I consider let/in to have a
544:
Indicate which equality is meant by '=' in the following set expression. (It might be helpful anyway throughout the whole article to use different characters for syntactic equality of lambda terms and for the 'mathematical interpretation', i.e. for equality modulo beta and eta reduction.) Also note
708:
I have changed the wording to hopefully clarify the issue. There is no actual problem with the lambda calculus domain, considered as a set, but if you add functions that are not defined on themselves, you get a contradiction. Interested in your comments on this and if there is a better approach
671:
My point is that the two functions given are extensionally equal but not intensionally equal. The two functions applied to church numerals will get the same result. But the two functions not applied to any parameter cannot beta reduce further and are therefore not equal, even though they are
490:
Thank you for your requests for clarification. Feel free to add clarification points and or add comments under talk, as you feel is best to make your point. I will address them as soon as I can. I really want the article to be correct and clear, so any input you make is greatly valued.
172:
472:
I liked to omit lengthy descriptions of the place I refer to (like "In the 3rd line from above in section 'No solutions', ..."). My vague overall impression of section "Logical inconsistency" is that if I could understand it, its point might be the same that is already made in
612:"In the mathematical interpretation, lambda terms represent values. Eta and beta reductions are deductive steps that do not alter the values of expressions." This makes beta and eta reduction not independent. Beta reduction is implied by eta reduction.
624:
3. "The left hand side may often be shown to be false where x = f" Nonsence: The x is placeholder, you cannnot substitute. Moreover, x is variable , f is lambda-term, so they are different syntactical categories.
805:
703:
The proof is only that there is no solution for F including a function that can not be applied to itself. So it does not completely rule out a set of function F. It just restricts it. What is your suggestion?
641:\r\s.2*(r+s) = \r\s.2*r + 2*s according to the distributive law these functions are extensionally equal. They are the same function. But they are different functions and not equal by intensional equality.
545:
that there is an untyped lambda term f such that (f f) evaluates to (¬ (f f)), viz. f = λx.(¬ (x x)). So it is not clear in which sense the set expression should be read in order to get cardinality 0.
563:
added remarks as clarify requests, cf. talk page; suggested parantheses to distinguish let equation x = (let f y =¬(y y) in f f ) from -nonsensical- equation chain x = (let f y) = (¬(y y) in f f ))
1319:
1149:
838:
function as well, which for positive resp. negative argument returns positive resp. negative root. (The n can be zero.) Or divergence for negative n - as in the previous example in the article.
196:
636:
2*(r + s) = r+s+r+s ?=? r+r+s+s = 2*r + 2*s, only if + is commutative. Functions aren't commutative. You have different functions, which sometimes give the same result. - for church numerals
408:
section is going to be too abstract and not useful to the general reader. I am trying to represent the viewpoint of a person studying pure untyped lambda calculus, but at a simple level.
1232:
1062:
336:
449:
Indicate clearly where the 'Logical inconsistency' mentioned in the section heading consists in. Having equations with zero or multiple solutions doesn't appear to be an inconsistency.
253:
191:
823:
7. "If not then the undecidability of equivalence shows that in general there is no algorithm to determine if two lambda terms are equal." - What it has to do with domains?
1384:
1379:
124:
114:
401:
section. I think it is important but I have not convinced myself or the reader that this is important. I would like to have some good references to read on this.
1389:
646:
I have changed the wording to hopefully clarify from the start that the two functions are not intensionally equal but the distributive law says they are equal.
90:
298:
687:"Therefore, if there exists a function that may not be applied to itself, then there is no set F satisfying the above definition of 'all functions'".
272:
137:
81:
58:
554:
The domain here is the real domain, not the lambda calculus domain of functions. I have attempted to clarify this in the terminology section.
513:
would be helpful to explain that 'y y' means (as I guess) function application of lambda terms, not multiplication of Church-encoded numbers.
361:
863:
244:
732:
225:
317:
444:
Indicate whether typed or untyped Lambda calculus is meant here. In untyped Lambda calculus, not every term has a normal form.
853:
But considered as an expression on signed numbers it represents two values in the domain of signed numbers (for non zero n).
1243:
1073:
282:
163:
33:
677:
5. "This definition is an unsolved equation for F. So is there a solution for F?" - Yes, it is. Single point F = {0}.
292:
206:
876:
I apologize for the delay in responding. I value your comments. I have tried to address them in the comments above.
617:
I moved the terminology section out into a separate section. Hopefully this will make the argument easier to follow.
694:
5a. As you don't rule out in the following this solution, the proof is incorrect (or incomplete). Try compare with
607:
from eta reduction, there is no contradiction between the two definitions." Rules \beta and \eta are indeopendent.
481:
327:
89:
related articles on
Knowledge. If you would like to participate, please visit the project page, where you can join
411:
I would really appreciate the input of lambda calculus mathematicians. I would like more references. What does
354:
867:
1181:
1011:
812:
I have said that g g is not in F, but not that g is not in f. Therefore I am entitled to instantiate x as g.
21:
942:
I don't recognise this term from secondary literature. Does it come from a reference that we can name? —
828:
If you can't decide if two expressions are equal how can you determine the set of elements in the domain?
477:
263:
39:
1355:
FV is short for Free
Variable. It is a meta-function that gives the free variables of an expression.
1360:
1331:
1161:
991:
928:
881:
714:
The set theoretic approach given here is similar to Rice's theorem. But it is simpler to understand
578:
498:
462:
425:
521:'y y' means function application. I have added a terminology section to hopefully clarify this.
182:
949:
473:
234:
86:
695:
524:
The numbers for this discussion are the reals. I am not considering Church encoding here.
412:
455:
a pure lambda calculus interpretation where every lambda term represents a single value.
1237:
leads to contradictions. What is the condition C on f that makes that definition valid?
1067:
leads to contradictions. What is the condition C on f that makes that definition valid?
1356:
1327:
1157:
987:
965:
960:
924:
877:
574:
494:
458:
421:
308:
150:
1364:
1335:
1165:
995:
969:
953:
932:
885:
871:
582:
502:
485:
466:
429:
173:
Requested articles/Applied arts and sciences/Computer science, computing, and
Internet
1373:
848:
Yes in the lambda calculus domain, it is one value by definition. It is what it is.
415:
say about this subject? I am hoping that the article can evolve from this start.
978:
illative ɪˈleɪtɪv/Submit adjective 1. of the nature of or stating an inference.
943:
418:
If any editors can suggest further reading I would be pleased to follow it up.
721:
6. "instantiate x as g." - You cannot, as you supposed that g g is undefined.
598:
Yes you can write it like that. It is not the notation used in this article.
215:
73:
52:
897:
653:
4a. Exaample is strange: Discriminate: functions values are the same for
551:
The equality is mathematical equality (see new
Terminology section).
570:
lower precedence than = but higher than equivalence, implication.
439:
Thanks for the requests for clarification. I have responded to,
900:. The Bulletin of Symbolic Logic, Volume 3, Number 2, June 1997.
898:
The Impact of the Lambda
Calculus in Logic and Computer Science
800:{\displaystyle f\in F\iff (\forall x:x\in F\implies f\ x\in F)}
291:
Find pictures for the biographies of computer scientists (see
15:
834:
two values in the signed number domain." - it represents
981:
Deductive seemed more accessible to the average reader.
921:
Request for the addition of a section on this subject.
630:
Restructured this section. The notation was confusing.
1246:
1184:
1076:
1014:
735:
85:, a collaborative effort to improve the coverage of
1314:{\displaystyle C(f)\iff (f\ x=y\iff f=\lambda x.y)}
1144:{\displaystyle C(f)\iff (f\ x=y\iff f=\lambda x.y)}
1313:
1226:
1143:
1056:
799:
197:Computer science articles needing expert attention
1348:X IS NOT IN IT THOUGH WHEN ETA REDUTION HAPPENS
337:WikiProject Computer science/Unreferenced BLPs
959:I'm fairly certain this term was invented by
8:
254:Computer science articles without infoboxes
192:Computer science articles needing attention
397:I have doubts about the usefulness of the
158:Here are some tasks awaiting attention:
132:
47:
1245:
1183:
1075:
1013:
734:
32:does not require a rating on Knowledge's
1385:Low-importance Computer science articles
1380:Redirect-Class Computer science articles
1288:
1283:
1264:
1259:
1227:{\displaystyle f\ x=y\iff f=\lambda x.y}
1204:
1199:
1118:
1113:
1094:
1089:
1057:{\displaystyle f\ x=y\iff f=\lambda x.y}
1034:
1029:
984:(interesting addition about omega-rule)
843:Yes for n not equal to zero, two values.
778:
773:
750:
745:
49:
99:Knowledge:WikiProject Computer science
1390:WikiProject Computer science articles
102:Template:WikiProject Computer science
79:This redirect is within the scope of
19:
7:
666:Not sure if I understand your point.
593:1. "\x.y z" usually means "\x(y z)"
938:Where does this material come from?
635:4. "2 * (r + s) = 2*r + 2*s" -: -->
38:It is of interest to the following
755:
273:Timeline of computing 2020–present
14:
817:And this leads to a contradiction
682:The proof does not rule this out.
299:Computing articles needing images
149:
119:This redirect has been rated as
72:
51:
20:
858:What change are you suggesting?
474:Curry's paradox#Lambda calculus
1308:
1285:
1266:
1261:
1256:
1250:
1201:
1138:
1115:
1096:
1091:
1086:
1080:
1031:
975:Curry used the term illative.
872:21:25, 18 September 2014 (UTC)
794:
775:
752:
747:
1:
933:18:17, 14 November 2014 (UTC)
657:versus (extensionality -: -->
538:I have reworked this section.
430:00:16, 22 February 2014 (UTC)
353:Tag all relevant articles in
93:and see a list of open tasks.
1324:Thanks for your assistance.
1154:Thanks for your assistance.
886:05:54, 30 October 2014 (UTC)
532:Is this a redefinition of x?
362:WikiProject Computer science
138:WikiProject Computer science
82:WikiProject Computer science
1336:21:47, 20 August 2016 (UTC)
1175:In general the definition,
1166:21:47, 20 August 2016 (UTC)
1005:In general the definition,
996:01:18, 20 August 2016 (UTC)
293:List of computer scientists
1406:
125:project's importance scale
1365:04:00, 11 July 2021 (UTC)
970:10:14, 16 June 2016 (UTC)
954:07:13, 16 June 2016 (UTC)
406:Domain of lambda calculus
404:I have concerns that the
355:Category:Computer science
131:
118:
105:Computer science articles
67:
46:
1345:NO ONE KNOWS WHAT FV IS
906:Illative lambda calculus
583:11:02, 21 May 2014 (UTC)
503:00:55, 21 May 2014 (UTC)
486:19:38, 20 May 2014 (UTC)
467:06:55, 19 May 2014 (UTC)
357:and sub-categories with
916:Illative lambda calculi
1315:
1228:
1145:
1058:
891:Request for assistance
801:
603:2. "As beta reduction
507:Clarification points,
394:This is a start only.
318:Computer science stubs
1316:
1229:
1146:
1059:
802:
1244:
1182:
1074:
1012:
733:
698:for usual approach.
672:extensionally equal.
399:Set theoretic domain
136:Things you can help
655:all church numerals
1311:
1289:
1284:
1265:
1260:
1224:
1205:
1200:
1141:
1119:
1114:
1095:
1090:
1054:
1035:
1030:
797:
779:
774:
751:
746:
34:content assessment
1273:
1189:
1103:
1019:
952:
896:Henk Barendregt,
784:
589:Anonymous remarks
392:
391:
388:
387:
384:
383:
380:
379:
376:
375:
1397:
1320:
1318:
1317:
1312:
1272:
1233:
1231:
1230:
1225:
1188:
1150:
1148:
1147:
1142:
1102:
1063:
1061:
1060:
1055:
1018:
948:
806:
804:
803:
798:
783:
660:all lambda terms
478:Jochen Burghardt
366:
360:
235:Computer science
164:Article requests
153:
146:
145:
133:
107:
106:
103:
100:
97:
96:Computer science
87:Computer science
76:
69:
68:
63:
59:Computer science
55:
48:
25:
24:
16:
1405:
1404:
1400:
1399:
1398:
1396:
1395:
1394:
1370:
1369:
1343:
1242:
1241:
1180:
1179:
1173:
1072:
1071:
1010:
1009:
1003:
945:Charles Stewart
940:
893:
731:
730:
591:
437:
372:
369:
364:
358:
346:Project-related
341:
322:
303:
277:
258:
239:
220:
201:
177:
104:
101:
98:
95:
94:
61:
12:
11:
5:
1403:
1401:
1393:
1392:
1387:
1382:
1372:
1371:
1368:
1367:
1342:
1339:
1322:
1321:
1310:
1307:
1304:
1301:
1298:
1295:
1292:
1287:
1282:
1279:
1276:
1271:
1268:
1263:
1258:
1255:
1252:
1249:
1235:
1234:
1223:
1220:
1217:
1214:
1211:
1208:
1203:
1198:
1195:
1192:
1187:
1172:
1169:
1152:
1151:
1140:
1137:
1134:
1131:
1128:
1125:
1122:
1117:
1112:
1109:
1106:
1101:
1098:
1093:
1088:
1085:
1082:
1079:
1065:
1064:
1053:
1050:
1047:
1044:
1041:
1038:
1033:
1028:
1025:
1022:
1017:
1002:
999:
973:
972:
961:User:Thepigdog
939:
936:
919:
918:
913:
908:
902:
901:
892:
889:
864:89.103.101.115
861:
860:
855:
850:
845:
831:
830:
821:
820:
814:
809:
808:
807:
796:
793:
790:
787:
782:
777:
772:
769:
766:
763:
760:
757:
754:
749:
744:
741:
738:
719:
718:
717:
716:
711:
696:Rice's theorem
692:
691:
690:
689:
675:
674:
668:
651:
650:
649:
648:
633:
632:
622:
621:
620:
619:
601:
600:
590:
587:
586:
572:
571:
566:
565:
556:
555:
552:
548:
547:
540:
539:
535:
534:
528:
527:
526:
525:
522:
516:
515:
452:
451:
446:
436:
433:
390:
389:
386:
385:
382:
381:
378:
377:
374:
373:
371:
370:
368:
367:
350:
342:
340:
339:
333:
323:
321:
320:
314:
304:
302:
301:
296:
288:
278:
276:
275:
269:
259:
257:
256:
250:
240:
238:
237:
231:
221:
219:
218:
212:
202:
200:
199:
194:
188:
178:
176:
175:
169:
157:
155:
154:
142:
141:
129:
128:
121:Low-importance
117:
111:
110:
108:
91:the discussion
77:
65:
64:
62:Low‑importance
56:
44:
43:
37:
26:
13:
10:
9:
6:
4:
3:
2:
1402:
1391:
1388:
1386:
1383:
1381:
1378:
1377:
1375:
1366:
1362:
1358:
1354:
1353:
1352:
1349:
1346:
1340:
1338:
1337:
1333:
1329:
1325:
1305:
1302:
1299:
1296:
1293:
1290:
1280:
1277:
1274:
1269:
1253:
1247:
1240:
1239:
1238:
1221:
1218:
1215:
1212:
1209:
1206:
1196:
1193:
1190:
1185:
1178:
1177:
1176:
1170:
1168:
1167:
1163:
1159:
1155:
1135:
1132:
1129:
1126:
1123:
1120:
1110:
1107:
1104:
1099:
1083:
1077:
1070:
1069:
1068:
1051:
1048:
1045:
1042:
1039:
1036:
1026:
1023:
1020:
1015:
1008:
1007:
1006:
1000:
998:
997:
993:
989:
985:
982:
979:
976:
971:
968:
967:
962:
958:
957:
956:
955:
951:
947:
946:
937:
935:
934:
930:
926:
922:
917:
914:
912:
909:
907:
904:
903:
899:
895:
894:
890:
888:
887:
883:
879:
874:
873:
869:
865:
859:
856:
854:
851:
849:
846:
844:
841:
840:
839:
837:
829:
826:
825:
824:
818:
815:
813:
810:
791:
788:
785:
780:
770:
767:
764:
761:
758:
742:
739:
736:
729:
728:
727:
724:
723:
722:
715:
712:
710:
706:
705:
704:
701:
700:
699:
697:
688:
685:
684:
683:
680:
679:
678:
673:
669:
667:
664:
663:
662:
661:
656:
647:
644:
643:
642:
639:
638:
637:
631:
628:
627:
626:
618:
615:
614:
613:
610:
609:
608:
606:
599:
596:
595:
594:
588:
585:
584:
580:
576:
568:
567:
564:
561:
560:
559:
553:
550:
549:
546:
542:
541:
537:
536:
533:
530:
529:
523:
520:
519:
518:
517:
514:
510:
509:
508:
505:
504:
500:
496:
492:
488:
487:
483:
479:
475:
469:
468:
464:
460:
456:
450:
447:
445:
442:
441:
440:
435:Clarification
434:
432:
431:
427:
423:
419:
416:
414:
409:
407:
402:
400:
395:
363:
356:
352:
351:
349:
347:
343:
338:
335:
334:
332:
330:
329:
324:
319:
316:
315:
313:
311:
310:
305:
300:
297:
294:
290:
289:
287:
285:
284:
279:
274:
271:
270:
268:
266:
265:
260:
255:
252:
251:
249:
247:
246:
241:
236:
233:
232:
230:
228:
227:
222:
217:
214:
213:
211:
209:
208:
203:
198:
195:
193:
190:
189:
187:
185:
184:
179:
174:
171:
170:
168:
166:
165:
160:
159:
156:
152:
148:
147:
144:
143:
139:
135:
134:
130:
126:
122:
116:
113:
112:
109:
92:
88:
84:
83:
78:
75:
71:
70:
66:
60:
57:
54:
50:
45:
41:
35:
31:
27:
23:
18:
17:
1350:
1347:
1344:
1326:
1323:
1236:
1174:
1156:
1153:
1066:
1004:
986:
983:
980:
977:
974:
964:
944:
941:
923:
920:
915:
911:Type systems
910:
905:
875:
862:
857:
852:
847:
842:
835:
832:
827:
822:
816:
811:
725:
720:
713:
707:
702:
693:
686:
681:
676:
670:
665:
659:
654:
652:
645:
640:
634:
629:
623:
616:
611:
604:
602:
597:
592:
573:
562:
557:
543:
531:
511:
506:
493:
489:
470:
457:
453:
448:
443:
438:
420:
417:
410:
405:
403:
398:
396:
393:
345:
344:
328:Unreferenced
326:
325:
307:
306:
281:
280:
262:
261:
243:
242:
224:
223:
205:
204:
181:
180:
162:
161:
120:
80:
40:WikiProjects
29:
1374:Categories
1351:THANK YOU
605:is implied
413:Barendregt
1357:Thepigdog
1328:Thepigdog
1158:Thepigdog
988:Thepigdog
925:Thepigdog
878:Thepigdog
575:Thepigdog
558:Comment:
495:Thepigdog
459:Thepigdog
422:Thepigdog
216:Computing
1341:WHATS FV
1171:Question
1001:Question
264:Maintain
207:Copyedit
30:redirect
726:I have,
245:Infobox
183:Cleanup
123:on the
950:(talk)
658:) for
226:Expand
36:scale.
709:here.
309:Stubs
283:Photo
140:with:
28:This
1361:talk
1332:talk
1162:talk
992:talk
966:Ruud
929:talk
882:talk
868:talk
579:talk
499:talk
482:talk
476:. -
463:talk
426:talk
963:. —
836:the
115:Low
1376::
1363:)
1334:)
1297:λ
1286:⟺
1262:⟺
1213:λ
1202:⟺
1164:)
1127:λ
1116:⟺
1092:⟺
1043:λ
1032:⟺
994:)
931:)
884:)
870:)
789:∈
776:⟹
768:∈
756:∀
748:⟺
740:∈
581:)
501:)
484:)
465:)
428:)
365:}}
359:{{
1359:(
1330:(
1309:)
1306:y
1303:.
1300:x
1294:=
1291:f
1281:y
1278:=
1275:x
1270:f
1267:(
1257:)
1254:f
1251:(
1248:C
1222:y
1219:.
1216:x
1210:=
1207:f
1197:y
1194:=
1191:x
1186:f
1160:(
1139:)
1136:y
1133:.
1130:x
1124:=
1121:f
1111:y
1108:=
1105:x
1100:f
1097:(
1087:)
1084:f
1081:(
1078:C
1052:y
1049:.
1046:x
1040:=
1037:f
1027:y
1024:=
1021:x
1016:f
990:(
927:(
880:(
866:(
819:.
795:)
792:F
786:x
781:f
771:F
765:x
762::
759:x
753:(
743:F
737:f
577:(
497:(
480:(
461:(
424:(
348::
331::
312::
295:)
286::
267::
248::
229::
210::
186::
167::
127:.
42::
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
