حساب لاندا، زبان ذهن، خواب

نامرتبه و کامل نیست. اما چون مقاله جالبی بود گفتم یه بخشایی رو ترجمه کنم.
اسم مقاه اینه: حساب لاندا، بازسازی برج بابل!
اسم نویسندش: David Perrin

گالیله به آدما گفت شما مرکز دنیا نیستید. داروین بشون گفت شما از حیوانات برتر نیستید. فروید بشون گفت شما اختیار کامل رفتارتون رو ندارید. نفر بعدی احتمالاً بشون میگه مغز شما از مدارهای الکتریکیه کامپیوتر خونگیتون پیشرفته تر نیست!

منظقدان فرانسوی، ژان لویی کریوین، Jean-Louis Krivine، سال 1997 ثابت کرد حساب لاندا توانایی بیان تمام استدلالها و تمام ساختارهای ریاضی ممکن رو داره.

%20HE02%20-%20Dossier%2C%20Le%20lambda%20calcul

تناظر Curry-Howard
بعد از Haskell Curry افراد دیگه ای تلاش کردن این فرهنگ لغت ریاضی-انفورماتیکی رو کامل کنن. اما این تناظر اونقدر گسترده نبود که توجه ریاضیدانای زیادی رو بخودش جلب کنه. برای مثال هیچ معادلی برای «برهان خلف» که یکی از راه های رایج اثبات قضایا تو ریاضیاته، وجود نداشت. برای مدت زیادی همه فکر میکردن فقط استدلالهایی که توشون از برهان خلف استفاده نشده رو میشه با حساب لاندا بیان کرد.
سال 1990 دو انفورماتیست آمریکایی، Matthias Felleisen و Timothy Griffin تونستن بالاخره معادل برهان خلف رو پیدا کنن. چیزی که تو تقریباً همه کامپیوترا وجود داشت: دستور EXIT. مثلاً وقتی از یه کامپیوتر میخوایید درایو دیویدی رو باز کنه درحالی که هیچ دیویدی ای تو دستگاه نزاشتین، این برنامه اجرا میشه و شما پیام خطا مشاهده میکنید. به طور کلی، این نوع برنامه ها یه وضعیت یا حالت خاصی از دستگاه رو ذخیره میکنن و در صورت بروز مشکل به اون وضعیت برمیگردن.

حالا که میشد همه نوع استدلال رو انجام داد، کریوین تلاش کرد چنتا قضیه معروف رو با حساب لاندا بیان کنه. برای این کار سراغ قضیه تمامیت گودل رفت. بعد به عبارت لاندای مربوط به قضیه تمامیت گودل به چشم یه برنامه کامپیوتری نگاه کرد و یجورایی نیمه پنهانشو دید.

برهان گودل در واقع نرم افزاری بود که برای خیلیا آشناست: Disassembler. این نرم افزار خط به خط یا درستترش دستور به دستور برنامه های دیگه رو اجرا میکنه تا کدشون رو بفهمه، کد رو تغییر بده یا خطاهای احتمالی برنامه نویسی رو پیدا کنه.

مثال!
image

اما طبق تعریف این نرم افزارها باید قدم به قدم دستورای برنامه مورد نظرو بررسی و اجرا کنن، مگر وقتی به دستور exit میرسن. یعنی باید بطور اتوماتیک این دستورها رو نادیده بگیرن. نمیشه از یه Disassembler انتظار داشت مرحله به مرحله دستورهای نوع exit رو اجرا کنه، چون باعث میشه کامپوتر هنگ کنه!

در واقع گودل وقتی هنوز کامپیوتری وجود نداشت یه برنامه نوشته که مربوط به امنیت سیستم میشه و برای کارکرد درست همین کامپوترای خونگی هم ضروری محسوب میشه، اما انگار کارکرد این برنامه با ایده ریاضی ای که پشتش بود هیچ ربطی نداره. و چون اونموقع هنوز خبری از کامپوتر نبود، این برنامه رو فقط میشد به یه چیز ربط داد و اونم ذهن بود.

کریوین نظریه ای داره که میگه این برنامه باید تو مغز ما هم وجود داشته باشه و وقتی مغز داره اجراش میکنه خودش باید غیر قابل استفاده بشه! این برنامه چی میتونه باشه؟ کریوین میگه این برنامه میتونه یکی از کارایی باشه که خواب انجام میده. گودل خیال میکرد محدودیتهای ریاضیات رو بررسی میکنه، خیال میکرد داره میگه رویای داوید هیلبرت (رسیدن به همه حقایق ریاضی با استفاده از چنتا اصل موضوع و قواعد ابتدایی) هیچوقت محقق نمیشه، اما در واقع داشت کارکرد ذهن خودشو بررسی میکرد. یجورایی میشه گفت داشت یه برنامه خیلی مهم برای روانکاوی مینوشت.

با این تعابیر خواب دیدن راهی برای بازیابی فایلهای مغزمونه که درست بسته نشدن.شب موقع خواب، برنامه ها مرتب میشن و اپلیکیشنهایی که کامل ازشون خارج نشدیم بسته میشن.

در واقع همه ریاضیدانها برنامه نویس هستن. اونا خیال میکردن دارن قضایای یه دنیای خیالی و ایده آل رو اثبات میکنن. ولی وقتی میشه تمام استدلال ها رو با حساب لاندا بیان کرد، و وقتی حساب لاندا یه زبان برنامه نویسی هم محسوب میشه، پس در واقع اثبات قضایا کدهای برنامه های کامپوتری هستن.

image

3 Likes

چیز عجیب غریبی بود