इस फ़ंक्शन का प्रकार क्यों है (ए -> ए) -> ए?

Question

इस फ़ंक्शन का प्रकार क्यों है (ए -> ए) -> ए?

Prelude> let y f = f (y f) 
Prelude> :t y 
y :: (t -> t) -> t 

यह एक अनंत/रिकर्सिव प्रकार नहीं होना चाहिए? मैं कोशिश करने जा रहा था और शब्दों में डाल रहा था जो मुझे लगता है कि यह प्रकार होना चाहिए, लेकिन मैं इसे किसी कारण से नहीं कर सकता।

y :: (t -> t) -> ?WTFIsGoingOnOnTheRHS? 

मुझे नहीं पता कि कैसे f (y f) किसी मान को हल करता है। निम्नलिखित मुझे थोड़ा और समझ में आता है:

Prelude> let y f x = f (y f) x 
Prelude> :t y 
y :: ((a -> b) -> a -> b) -> a -> b 

लेकिन यह अभी भी हास्यास्पद रूप से भ्रमित है। क्या चल रहा है?

Answer 1

खैर, y, कुछ a, b और c हम अभी तक पता नहीं के लिए प्रकार (a -> b) -> c का हो गया है; आखिरकार, यह एक फ़ंक्शन लेता है, f, और इसे एक तर्क पर लागू करता है, इसलिए यह एक फ़ंक्शन लेने वाला फ़ंक्शन होना चाहिए।

y f = f x के बाद से (फिर से, कुछ x के लिए), हम जानते हैं कि y की वापसी प्रकार f खुद की वापसी प्रकार होना चाहिए। इसलिए, हम y के प्रकार को थोड़ा सा परिशोधित कर सकते हैं: कुछ a और b के लिए हमें अभी तक पता नहीं है।

यह पता लगाने के लिए कि a क्या है, हमें केवल f पर दिए गए मान के प्रकार को देखना होगा। यह y f है, जो अभिव्यक्ति है जिसे हम अभी इस प्रकार का पता लगाने की कोशिश कर रहे हैं। हम कह रहे हैं कि y का प्रकार (a -> b) -> b है (कुछ a, b इत्यादि के लिए), इसलिए हम कह सकते हैं कि y f का यह एप्लिकेशन b प्रकार का होना चाहिए।

तो, f को तर्क के प्रकार b है। इसे सब एक साथ वापस रखो, और हमें (b -> b) -> b मिलता है - जो निश्चित रूप से (a -> a) -> a जैसा ही है।

यहाँ चीजों के एक अधिक सहज ज्ञान युक्त है, लेकिन कम सटीक दृश्य है: हम कह रहे हो कि y f = f (y f) है, जो हम बराबर y f = f (f (y f)), y f = f (f (f (y f))) लिए विस्तार कर सकते हैं, और इतने पर। तो, हम जानते हैं कि हम हमेशा पूरी बात के चारों ओर एक और f आवेदन कर सकते हैं, और "पूरी बात" प्रश्न में के बाद से एक तर्क को f लागू करने का परिणाम है, f प्रकार a -> a के लिए है; और चूंकि हमने अभी निष्कर्ष निकाला है कि पूरी बात f को तर्क के लिए लागू करने का परिणाम है, y का रिटर्न प्रकार f स्वयं होना चाहिए - फिर से, (a -> a) -> a के रूप में एक साथ आना चाहिए।

Answer 2

@ एहर्ड ने इस प्रकार को समझाने का अच्छा काम किया है, इसलिए मैं यह दिखाना चाहता हूं कि यह कुछ उदाहरणों के साथ किसी मूल्य को कैसे हल कर सकता है।

f1 :: Int -> Int 
f1 _ = 5 

-- expansion of y applied to f1 
y f1 
f1 (y f1) -- definition of y 
5   -- definition of f1 (the argument is ignored) 

-- here's an example that uses the argument, a factorial function 
fac :: (Int -> Int) -> (Int -> Int) 
fac next 1 = 1 
fac next n = n * next (n-1) 

y fac :: Int -> Int 
fac (y fac) -- def. of y 
    -- at this point, further evaluation requires the next argument 
    -- so let's try 3 
fac (y fac) 3 :: Int 
3 * (y fac) 2    -- def. of fac 
3 * (fac (y fac) 2)  -- def. of y 
3 * (2 * (y fac) 1)  -- def. of fac 
3 * (2 * (fac (y fac) 1) -- def. of y 
3 * (2 * 1)    -- def. of fac 

आप किसी भी कार्य के साथ उसी चरण का पालन कर सकते हैं जो आप देखना चाहते हैं कि क्या होगा। इन दोनों उदाहरणों के मूल्यों में अभिसरण है, लेकिन यह हमेशा नहीं होता है।

Answer 3

मुझे एक संयोजक के बारे में बताना है।यह "fixpoint Combinator" कहा जाता है और यह निम्नलिखित गुण:

संपत्ति: "fixpoint Combinator" एक समारोह f :: (a -> a) और पता चलता है एक "नियत बिन्दु" कि समारोह ऐसा है कि f x == x की x :: a लेता है। फिक्सपॉइंट संयोजक के कुछ कार्यान्वयन "खोज" पर बेहतर या बदतर हो सकते हैं, लेकिन यह मानते हुए कि यह समाप्त हो जाता है, यह इनपुट फ़ंक्शन का एक निश्चित बिंदु उत्पन्न करेगा। संपत्ति को संतुष्ट करने वाला कोई भी कार्य "फिक्सपॉइंट संयोजक" कहलाता है।

इस "फिक्सपॉइंट संयोजक" y पर कॉल करें। हमने जो कहा है उसके आधार पर, निम्नलिखित सत्य हैं:

-- as we said, y's input is f :: a -> a, and its output is x :: a, therefore 
y :: (a -> a) -> a 

-- let x be the fixed point discovered by applying f to y 
y f == x -- because y discovers x, a fixed point of f, per The Property 
f x == x -- the behavior of a fixed point, per The Property 

-- now, per substitution of "x" with "f x" in "y f == x" 
y f == f x 
-- again, per substitution of "x" with "y f" in the previous line 
y f == f (y f) 

तो वहां आप जाते हैं। फिक्सपॉइंट संयोजक की आवश्यक संपत्ति के संदर्भ में आपके पास परिभाषितy है:
y f == f (y f)। यह मानने के बजाय कि y fx पता चलता है, आप मान सकते हैं कि x एक अलग गणना का प्रतिनिधित्व करता है, और फिर भी एक ही निष्कर्ष (iinm) पर आता है।

चूंकि आपका कार्य संपत्ति को संतुष्ट करता है, हम निष्कर्ष निकाल सकते हैं कि यह एक फिक्सपॉइंट संयोजक है, और अन्य गुण जो हमने कहा है, सहित, आपके कार्य पर लागू होते हैं।

यह बिल्कुल ठोस प्रमाण नहीं है, लेकिन मुझे उम्मीद है कि यह अतिरिक्त अंतर्दृष्टि प्रदान करेगी।

Answer 4

अन्य लोगों के उत्तरों में जोड़ने के लिए केवल दो अंक।

समारोह आप तय कर रहे हैं आमतौर पर fix कहा जाता है, और यह एक fixed-point combinator है: एक समारोह है कि एक और समारोह के fixed point गणना करता है। गणित में, f फ़ंक्शन का निश्चित बिंदु x है जो f x = x है। यह आपको पहले से यह अनुमान लगाने की अनुमति देता है कि fix का प्रकार (a -> a) -> a होना चाहिए; "फ़ंक्शन जो a से a पर फ़ंक्शन लेता है, और a देता है।"

आप अपने समारोह y, जो Y combinator के बाद हो रहा है कहा जाता है, लेकिन इस एक गलत नाम है: Y Combinator एक विशिष्ट निश्चित बिंदु Combinator, लेकिन एक द्वारा निर्धारित किए गए के समान नहीं है यहाँ।

मुझे नहीं पता कि कैसे f (y f) किसी मान को हल करता है।

ठीक है, चाल यह है कि हास्केल एक गैर-सख्त (ए.के.ए. "आलसी") भाषा है। की गणना f को सभी मामलों में y f तर्क का मूल्यांकन करने की आवश्यकता नहीं है। इसलिए, यदि आप फैक्टोरियल को परिभाषित कर रहे हैं (जैसा कि जॉन एल चित्रित करता है), fac (y fac) 1y fac का मूल्यांकन किए बिना 1 का मूल्यांकन करता है।

सख्त भाषाएं ऐसा नहीं कर सकती हैं, इसलिए उन भाषाओं में आप इस तरह से एक निश्चित बिंदु संयोजक को परिभाषित नहीं कर सकते हैं। उन भाषाओं में, पाठ्यपुस्तक निश्चित-बिंदु संयोजक वाई संयोजक उचित है।