جبر لاندا: تفاوت میان نسخه‌ها
محتوای حذف‌شده محتوای افزوده‌شده
جز ربات: انتقال رده به درخواست Modern Sciences از رده:اختراعات آمریکایی به رده:اختراعهای آمریکایی |
|||
خط ۳۷:
== تعریف و کاربرد ==
جبر لاندا یک [[کامل بودن تورینگ|
جبر لاندا می‌تواند ''نوع‌دار'' (Typed) یا ''بدون نوع'' (Untyped) باشد. در جبر لاندای نوع‌دار یک تابع درصورتی می‌تواند صدا زده شود که توانایی پذیرش داده‌هایی با آن «[[نوع داده|نوع]]» خاص را داشته باشد. جبرهای لاندا نوع‌دار از لحاظ محاسباتی توانایی بیان کردن کمتری از جبرهای لاندای بدون نوع دارند؛ لذا از این جهت ضعیف‌تر هستند. اما از سوی دیگر قابلیت اثبات بالاتری دارند و می‌توانند چیزهای بیشتری را اثبات کنند. برای مثال در جبر لاندای نوع‌دار ساده، تمامی استراتژی‌های محاسبه تمام‌شدنی (terminating) هستند؛ در حالی که در جبر بدون نوع نیازی به تمام شدنی بودن نیست و محاسبه یک عبارت می‌تواند تا بینهایت ادامه پیدا کند.
| |||