كيف يمكنني تعريف y-combinator دون "Let Rec"؟

Question

في جميع الأمثلة تقريبًا ، تتم كتابة كومبيني Y في لغات ML من النوع على هذا النحو:

let rec y f x = f (y f) x
let factorial = y (fun f -> function 0 -> 1 | n -> n * f(n - 1))

يعمل هذا كما هو متوقع ، لكنه يبدو وكأنه غش في تحديد y-combinator باستخدام let rec ....

أرغب في تحديد هذا combinator دون استخدام عودة ، باستخدام التعريف القياسي:

Y = λf·(λx·f (x x)) (λx·f (x x))

الترجمة المباشرة هي كما يلي:

let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;

ومع ذلك ، يشكو F# من أنه لا يمكن معرفة الأنواع:

  let y = fun f -> (fun x -> f (x x)) (fun x -> f (x x));;
  --------------------------------^

C:\Users\Juliet\AppData\Local\Temp\stdin(6,33): error FS0001: Type mismatch. Expecting a
    'a    
but given a
    'a -> 'b    
The resulting type would be infinite when unifying ''a' and ''a -> 'b'

كيف أكتب y-combinator في f# دون استخدام let rec ...?

Answer 1

كما يشير المترجم ، لا يوجد نوع يمكن تعيينه إليه x بحيث التعبير (x x) غامضة (هذا ليس صحيحًا تمامًا ؛ يمكنك الكتابة صراحة x كما obj->_ - انظر فقرتي الأخيرة). يمكنك العمل حول هذه المشكلة من خلال إعلان نوع عودية حتى يعمل تعبير مشابه جدًا:

type 'a Rec = Rec of ('a Rec -> 'a)

الآن يمكن كتابة y-combinator على النحو التالي:

let y f =
  let f' (Rec x as rx) = f (x rx)
  f' (Rec f')

لسوء الحظ ، ستجد أن هذا ليس مفيدًا للغاية لأن F# هي لغة صارمة ، لذا فإن أي وظيفة تحاول تحديدها باستخدام هذا combinator ستتسبب في تدفق مكدس. بدلاً من ذلك ، تحتاج إلى استخدام الإصدار التطبيقي من y-combinator (\f.(\x.f(\y.(x x)y))(\x.f(\y.(x x)y))):

let y f =
  let f' (Rec x as rx) = f (fun y -> x rx y)
  f' (Rec f')

هناك خيار آخر هو استخدام الكسل الصريح لتحديد المركب Y العادي:

type 'a Rec = Rec of ('a Rec -> 'a Lazy)
let y f =
  let f' (Rec x as rx) = lazy f (x rx)
  (f' (Rec f')).Value

هذا له عيب مفاده أن تعريفات الوظائف العودية تحتاج الآن إلى قوة صريحة من القيمة الكسولة (باستخدام Value منشأه):

let factorial = y (fun f -> function | 0 -> 1 | n -> n * (f.Value (n - 1)))

ومع ذلك ، فإنه يتمتع بميزة أنه يمكنك تحديد قيم عودية غير وظيفية ، تمامًا كما تستطيع في لغة كسول:

let ones = y (fun ones -> LazyList.consf 1 (fun () -> ones.Value))

كبديل نهائي ، يمكنك محاولة تقريبية حساب حساب Lambda غير الصغير بشكل أفضل باستخدام الملاكمة والتعب. هذا من شأنه أن يمنحك (مرة أخرى باستخدام النسخة التطبيقية من y-combinator):

let y f =
  let f' (x:obj -> _) = f (fun y -> x x y)
  f' (fun x -> f' (x :?> _))

هذا له عيب واضح هو أنه سيتسبب في ملاكمة غير ضرورية وملاكمة ، ولكن على الأقل هذا داخلي تمامًا للتنفيذ ولن يؤدي فعليًا إلى الفشل في وقت التشغيل.

Answer 2

أود أن أقول إنه أمر مستحيل ، وسألني عن السبب ، كنت سأستدعى حقيقة أن حساب حساب Lambda الذي كتب ببساطة يحتوي على خاصية التطبيع. باختصار ، جميع شروط حساب حساب Lambda المكتوب ببساطة (وبالتالي لا يمكن تعريف Y في حساب Lambda المكتوب ببساطة).

نظام نوع F#ليس بالضبط نظام حساب حساب Lambda المكتوب ببساطة ، لكنه قريب بما فيه الكفاية. و# بدون let rec يقترب حقًا من حساب Lambda الذي تم كتابته ببساطة - ولتكرار ، في تلك اللغة ، لا يمكنك تحديد مصطلح لا ينتهي ، ويستبعد تحديد Y أيضًا.

بمعنى آخر ، في F#، يجب أن تكون "Let Rec" لغة بدائية على الأقل لأنه حتى لو تمكنت من تعريفه من البدائية الأخرى ، فلن تتمكن من كتابة هذا التعريف. إن امتلاكه كبداية يتيح لك ، من بين أشياء أخرى ، إعطاء نوع خاص لذلك البدائي.

تحرير: يظهر KVB في إجابته أن تعريفات النوع (إحدى الميزات التي تغيب عن Lambda-Calculus المكتوبة ببساطة ولكنها موجودة في Let-Rec-less F#) تسمح بالحصول على نوع من العودية. ذكي جدا.

Answer 3

العلبة والسماح للبيانات في مشتقات ML هي ما يجعلها كاملة ، وأعتقد أنها تستند إلى النظام F وليس الكتابة ببساطة ولكن النقطة هي نفسها.

لا يمكن للنظام F العثور على نوع لأي مجموعة من النقاط الثابتة ، إذا كان بإمكانه ذلك ، لم يكن طبيعًا بقوة.

ما يعنيه التطبيع بقوة هو أن أي تعبير لديه بالضبط واحد الشكل الطبيعي ، حيث يكون الشكل الطبيعي عبارة عن تعبير لا يمكن تقليله أكثر من ذلك في ماكس شكل عادي واحد ، كما يمكن أن لا يوجد شكل عادي على الإطلاق.

إذا تمكنت حساب Lambda Calculi من بناء مشغل نقاط ثابتة بأي طريقة من أي وقت مضى ، فقد كان من الممكن أن يكون للتعبير أي شكل عادي.

نظرية أخرى مشهورة ، وهي مشكلة توقف ، تعني أن اللغات التطبيع بقوة ليست كاملة ، فهي تقول إن هذا مستحيل قرر (مختلف عن إثبات) لغة كاملة ، ستتوقف مجموعة فرعية من برامجها على الإدخال. إذا كانت اللغة تتطبيع بقوة ، فهي قابلة للتخلص من ذلك إذا توقفت ، أي دائماً توقف. خوارزميةنا لتقرر أن هذا هو البرنامج: true;.

لحل هذا ، تمديد المستثمرات ML System-F مع CASE ودع (REC) للتغلب على هذا. وبالتالي ، يمكن للوظائف أن تشير إلى نفسها في تعريفاتها مرة أخرى ، مما يجعلها سارية المفعول لا حساب Lambda على الإطلاق ، لم يعد من الممكن الاعتماد على الوظائف المجهولة وحدها لجميع الوظائف الحاسوبية. يمكنهم بالتالي إدخال حلقات لا حصر لها واستعادة اكتمالهم.

Answer 4

إجابة قصيرة: لا يمكنك.

إجابة طويلة: حساب Lambda المكتوب ببساطة يتطبيع بقوة. هذا يعني أنه ليس مكافئًا. يتلخص سبب هذا الأمر بشكل أساسي في حقيقة أن combinator يجب أن يكون بدائيًا أو محددًا بشكل متكرر (كما وجدت). لا يمكن التعبير عنها ببساطة في النظام F (أو حساب أكسيد أبسط). لا توجد طريقة للتغلب على هذا (لقد ثبت ، بعد كل شيء). y combinator لك يستطيع ينفذ التنفيذ بالضبط بالطريقة التي تريدها ، رغم ذلك.

أود أن أقترح عليك تجربة المخطط إذا كنت تريد مجموعة حقيقية على غرار الكنيسة. استخدم الإصدار التطبيقي الوارد أعلاه ، حيث لن تعمل الإصدارات الأخرى ، إلا إذا قمت بإضافة الكسل بشكل صريح ، أو استخدام مترجم مخطط كسول. (المخطط من الناحية الفنية غير مقلوب تمامًا ، ولكنه مكتوب ديناميكيًا ، وهو أمر جيد بما يكفي لهذا.)

انظر هذا لدليل التطبيع القوي:http://citeseerx.ist.psu.edu/viewdoc/summary؟doi=10.1.1.127.1794

بعد التفكير أكثر من ذلك ، أنا متأكد تمامًا من أن إضافة combinator بدائي يتصرف تمامًا بالطريقة التي يحدد بها LetRec الذي يجعل النظام مكتملًا. كل ما عليك القيام به لمحاكاة آلة turing ثم يتم تنفيذ الشريط كصبع صحيح (يتم تفسيره في الثنائي) والتحول (لوضع الرأس).