Hindley–Milner type system
હિન્ડલી-મિલનર (એચ. એમ.) પ્રકારની પ્રણાલી એ પેરામેટ્રિક પોલીમોર્ફિઝમ સાથે લેમ્બડા કલન માટે એક શાસ્ત્રીય પ્રકારની પ્રણાલી છે. તેને દમાસ-મિલ્નર અથવા દમાસ-હિન્ડલી-મિલ્નર તરીકે પણ ઓળખવામાં આવે છે. તેનું વર્ણન સૌપ્રથમ જે. રોજર હિન્દલી દ્વારા કરવામાં આવ્યું હતું અને બાદમાં રોબિન મિલ્નર દ્વારા તેની પુનઃ શોધ કરવામાં આવી હતી. લુઇસ દામાસે તેમના પીએચડી થીસીસમાં નજીકના ઔપચારિક વિશ્લેષણ અને પદ્ધતિનો પુરાવો આપ્યો હતો. એચ. એમ. ના વધુ નોંધપાત્ર ગુણધર્મોમાં તેની સંપૂર્ણતા અને પ્રોગ્રામર દ્વારા પૂરી પાડવામાં આવેલ પ્રકારની ટિપ્પણીઓ અથવા અન્ય સંકેતો વિના આપેલ પ્રોગ્રામના સૌથી સામાન્ય પ્રકારનું અનુમાન કરવાની તેની ક્ષમતા છે. અલ્ગોરિધમ W એ વ્યવહારમાં એક કાર્યક્ષમ પ્રકારની અનુમાન પદ્ધતિ છે અને મોટા કોડ પાયા પર સફળતાપૂર્વક લાગુ કરવામાં આવી છે, જો કે તેમાં ઉચ્ચ સૈદ્ધાંતિક જટિલતા છે. એચ. એમ. નો ઉપયોગ કાર્યાત્મક ભાષાઓ માટે પ્રાધાન્યમાં થાય છે. તે સૌપ્રથમ પ્રોગ્રામિંગ લેંગ્વેજ એમ. એલ. ની પ્રકાર પ્રણાલીના ભાગ રૂપે અમલમાં મૂકવામાં આવી હતી. ત્યારથી, એચ. એમ. ને વિવિધ રીતે વિસ્તૃત કરવામાં આવ્યું છે, ખાસ કરીને હાસ્કેલ જેવા પ્રકાર વર્ગની મર્યાદાઓ સાથે. પરિચય એક પ્રકારની અનુમાન પદ્ધતિ તરીકે, હિન્ડલી-મિલનર સંપૂર્ણપણે અનટાઈપ્ડ શૈલીમાં લખાયેલા પ્રોગ્રામ્સમાંથી ચલ, અભિવ્યક્તિઓ અને કાર્યોના પ્રકારો કાઢવામાં સક્ષમ છે. અવકાશ પ્રત્યે સંવેદનશીલ હોવાને કારણે, તે ફક્ત સ્રોત કોડના નાના ભાગમાંથી જ પ્રકારો મેળવવા સુધી મર્યાદિત નથી, પરંતુ સંપૂર્ણ કાર્યક્રમો અથવા મોડ્યુલોમાંથી મેળવવામાં આવે છે. પેરામેટ્રિક પ્રકારોનો સામનો કરવામાં પણ સક્ષમ હોવાથી, તે ઘણી કાર્યાત્મક પ્રોગ્રામિંગ ભાષાઓની પ્રકાર પ્રણાલીઓનો મુખ્ય ભાગ છે. તે સૌપ્રથમ એમ. એલ. પ્રોગ્રામિંગ ભાષામાં આ રીતે લાગુ કરવામાં આવ્યું હતું. મૂળ સરળ રીતે ટાઇપ કરેલા લેમ્બડા કેલ્ક્યુલસ માટે પ્રકાર અનુમાન અલ્ગોરિધમ છે જે 1958 માં હાસ્કેલ કરી અને રોબર્ટ ફેય્સ દ્વારા તૈયાર કરવામાં આવ્યું હતું. 1969 માં, જે. રોજર હિન્ડલીએ આ કાર્યને વિસ્તૃત કર્યું અને સાબિત કર્યું કે તેમના અલ્ગોરિધમનો હંમેશા સૌથી સામાન્ય પ્રકારનું અનુમાન કરે છે. 1978માં, રોબિન મિલ્નરે, હિન્દલીના કામથી સ્વતંત્ર રીતે, એક સમકક્ષ અલ્ગોરિધમ પ્રદાન કર્યું, એલ્ગોરિધમ ડબલ્યુ. 1982માં, લુઇસ દામાસે આખરે સાબિત કર્યું કે મિલ્નરનું અલ્ગોરિધમ પૂર્ણ છે અને તેને બહુરૂપી સંદર્ભો સાથેની સિસ્ટમોને ટેકો આપવા માટે વિસ્તૃત કર્યું. મોનોમોર્ફિઝમ વિ. પોલીમોર્ફિઝમ સરળ રીતે ટાઇપ કરેલા લેમ્બડા કેલ્ક્યુલસમાં, પ્રકારો અણુ પ્રકારનાં સ્થિરાંકો અથવા કાર્ય પ્રકારનાં સ્વરૂપો છે. આવા પ્રકારો મોનોમોર્ફિક છે. લાક્ષણિક ઉદાહરણો અંકગણિત મૂલ્યોમાં ઉપયોગમાં લેવાતા પ્રકારો છેઃ 3: સંખ્યા ઉમેરો 3 4: સંખ્યા ઉમેરોઃ સંખ્યા-> સંખ્યા-> સંખ્યા તેનાથી વિપરીત, અનટાઈપ્ડ લેમ્બડા કલન લખવા માટે બિલકુલ તટસ્થ છે, અને તેના ઘણા કાર્યો તમામ પ્રકારની દલીલો પર અર્થપૂર્ણ રીતે લાગુ કરી શકાય છે. તુચ્છ ઉદાહરણ એ ઓળખ કાર્ય આઈડી ષ્ણ λx છે. x જે જે પણ મૂલ્ય પર લાગુ થાય છે તે પરત કરે છે. ઓછા તુચ્છ ઉદાહરણોમાં સૂચિ જેવા પેરામેટ્રિક પ્રકારોનો સમાવેશ થાય છે. જ્યારે સામાન્ય રીતે બહુરૂપતાનો અર્થ એ છે કે કામગીરી એક કરતાં વધુ પ્રકારના મૂલ્યોને સ્વીકારે છે, ત્યારે અહીં વપરાયેલ બહુરૂપતાનો અર્થ પેરામેટ્રિક છે. સાહિત્યમાં પ્રકાર યોજનાઓના સંકેતો પણ જોવા મળે છે, જે બહુરૂપતાના પેરામેટ્રિક સ્વભાવ પર ભાર મૂકે છે. વધુમાં, અચળાંકોને (માત્રાત્મક) પ્રકારનાં ચલ સાથે ટાઇપ કરી શકાય છે. દા. ત. : વિપક્ષઃ બધા માટે a. a-> સૂચિ a-> સૂચિ a શૂન્યઃ બધા માટે a. એક ઓળખપત્રની યાદી બનાવોઃ forall a. a-> પોલીમોર્ફિક પ્રકારો તેમના ચલની સુસંગત અવેજી દ્વારા મોનોમોર્ફિક બની શકે છે. મોનોમોર્ફિક ઉદાહરણોના ઉદાહરણો છેઃ આઈડી ': શબ્દમાળા-> શબ્દમાળા શૂન્ય': સૂચિ સંખ્યા વધુ સામાન્ય રીતે, પ્રકારો બહુરૂપી હોય છે જ્યારે તેમાં પ્રકાર ચલ હોય છે, જ્યારે તેમના વિનાના પ્રકારો મોનોમોર્ફિક હોય છે. ઉદાહરણ તરીકે પાસ્કલ (1970) અથવા સી (1972) માં ઉપયોગમાં લેવાતી પ્રકાર પ્રણાલીઓથી વિપરીત, જે ફક્ત મોનોમોર્ફિક પ્રકારોને ટેકો આપે છે, એચ. એમ. ની રચના પેરામેટ્રિક પોલીમોર્ફિઝમ પર ભાર મૂકવાની સાથે કરવામાં આવી છે. ઉલ્લેખિત ભાષાઓના અનુગામીઓ, જેમ કે સી + + (1985), વિવિધ પ્રકારના બહુરૂપતા પર ધ્યાન કેન્દ્રિત કરે છે, એટલે કે ઓબ્જેક્ટ-ઓરિએન્ટેડ પ્રોગ્રામિંગ અને ઓવરલોડિંગના સંબંધમાં સબટાઇપિંગ. જ્યારે સબટાઇપિંગ એચ. એમ. સાથે અસંગત છે, ત્યારે હાસ્કેલની એચ. એમ. આધારિત પ્રકારની પ્રણાલીમાં વ્યવસ્થિત ઓવરલોડિંગનો એક પ્રકાર ઉપલબ્ધ છે. ચાલો-બહુરૂપતા જ્યારે બહુરૂપતા તરફ સરળ-ટાઇપ કરેલા લેમ્બડા કેલ્ક્યુલસ માટે પ્રકાર અનુમાન વિસ્તરે છે, ત્યારે વ્યક્તિએ વ્યાખ્યાયિત કરવું પડશે કે ક્યારે મૂલ્યનું ઉદાહરણ મેળવવું સ્વીકાર્ય છે. આદર્શ રીતે, આને બાઉન્ડ વેરિયેબલના કોઈપણ ઉપયોગ સાથે મંજૂરી આપવામાં આવશે, જેમ કેઃ (λid. . (આઈડી 3). (આઈડી "ટેક્સ્ટ").) (λx. x) કમનસીબે, બહુરૂપી લેમ્બડા કલનમાં પ્રકાર અનુમાન નિર્ણાયક નથી. તેના બદલે, એચ. એમ. આઈ. ડી. = λx સ્વરૂપનું લેટ-પોલીમોર્ફિઝમ પ્રદાન કરે છે. x in. (આઈ. ડી. 3). (આઈ. ડી. "લખાણ"). અભિવ્યક્તિ વાક્યરચનાના વિસ્તરણમાં બંધનકર્તા પદ્ધતિને મર્યાદિત કરે છે. માત્ર લેટ કન્સ્ટ્રક્ટમાં બંધાયેલા મૂલ્યો ત્વરિતતાને આધિન છે, એટલે કે. તે બહુરૂપી હોય છે, જ્યારે લેમ્બડા-એબ્સ્ટ્રેક્શનમાં પરિમાણોને મોનોમોર્ફિક ગણવામાં આવે છે. ઝાંખી આ લેખનો બાકીનો ભાગ નીચે પ્રમાણે આગળ વધે છેઃ એચ. એમ. પ્રકારની પ્રણાલી વ્યાખ્યાયિત કરવામાં આવી છે. આ એક કપાત પ્રણાલીનું વર્ણન કરીને કરવામાં આવે છે જે ચોક્કસ બનાવે છે કે કયા પ્રકારનાં અભિવ્યક્તિઓ છે, જો કોઈ હોય તો. ત્યાંથી, તે પ્રકાર અનુમાન પદ્ધતિના અમલીકરણ તરફ કામ કરે છે. ઉપરોક્ત ડિડક્ટિવ સિસ્ટમનો વાક્યરચના-સંચાલિત પ્રકાર રજૂ કર્યા પછી, તે એક કાર્યક્ષમ અમલીકરણ (અલ્ગોરિધમ જે) નું સ્કેચ કરે છે, જે મોટે ભાગે વાચકના ધાતુશાસ્ત્રીય અંતર્જ્ઞાનને આકર્ષિત કરે છે. કારણ કે તે ખુલ્લું રહે છે કે શું અલ્ગોરિધમ J ખરેખર પ્રારંભિક કપાત પ્રણાલીને અનુભવે છે, ઓછા કાર્યક્ષમ અમલીકરણ (અલ્ગોરિધમ W), રજૂ કરવામાં આવે છે અને સાબિતીમાં તેનો ઉપયોગ સંકેત આપવામાં આવે છે. છેવટે, અલ્ગોરિધમ સંબંધિત વધુ વિષયોની ચર્ચા કરવામાં આવે છે. એચ. એમ. પદ્ધતિ સીધી તુલનાત્મક રીતે રજૂ કરવામાં આવે છે તે વિવિધ સ્વરૂપો બનાવવા માટે, કપાત પદ્ધતિનું સમાન વર્ણન બે અલ્ગોરિધમ્સ માટે પણ વપરાય છે. હિન્ડલી-મિલનર પ્રકારની પ્રણાલી પ્રકાર પ્રણાલીને ઔપચારિક રીતે વાક્યરચના નિયમો દ્વારા વર્ણવી શકાય છે જે અભિવ્યક્તિઓ, પ્રકારો વગેરે માટે ભાષાને નિશ્ચિત કરે છે. અહીં આવા વાક્યરચનાની રજૂઆત ખૂબ ઔપચારિક નથી, જેમાં તે સપાટીના વ્યાકરણનો અભ્યાસ કરવા માટે નહીં, પરંતુ ઊંડાણપૂર્વકના વ્યાકરણનો અભ્યાસ કરવા માટે લખવામાં આવે છે, અને કેટલીક વાક્યરચના વિગતો ખુલ્લી રાખે છે. પ્રસ્તુતિનું આ સ્વરૂપ સામાન્ય છે. આના આધારે, અભિવ્યક્તિઓ અને પ્રકારો કેવી રીતે સંબંધિત છે તે નિર્ધારિત કરવા માટે ટાઇપિંગ નિયમોનો ઉપયોગ કરવામાં આવે છે. પહેલાની જેમ, વપરાયેલ સ્વરૂપ થોડું ઉદાર છે. વાક્યરચના ટાઇપ કરવા માટેની અભિવ્યક્તિઓ બરાબર તે જ છે જે અડીને આવેલા કોષ્ટકમાં બતાવ્યા પ્રમાણે લેમ્બડા કલનની અભિવ્યક્તિ સાથે વિસ્તૃત છે. અભિવ્યક્તિને અસ્પષ્ટ કરવા માટે કૌંસનો ઉપયોગ કરી શકાય છે. એપ્લિકેશન ડાબી બાજુથી બંધનકર્તા છે અને એબ્સ્ટ્રેક્શન અથવા લેટ-ઇન કન્સ્ટ્રક્ટ કરતાં વધુ મજબૂત રીતે બંધનકર્તા છે. પ્રકારોને વાક્યરચનાત્મક રીતે બે જૂથો, મોનોટાઇપ્સ અને પોલીટાઇપ્સમાં વહેંચવામાં આવે છે. મોનોટાઇપ્સ મોનોટાઇપ્સ હંમેશા ચોક્કસ પ્રકારને નિયુક્ત કરે છે. મોનોટાઇપ્સને વાક્યરચનામાં શબ્દો તરીકે રજૂ કરવામાં આવે છે. મોનોટાઇપ્સના ઉદાહરણોમાં અથવા જેવા પ્રકાર સ્થિરાંકો અને પેરામેટ્રિક પ્રકારોનો સમાવેશ થાય છે. પછીના પ્રકારો પ્રકાર કાર્યોના ઉપયોગોના ઉદાહરણો છે, ઉદાહરણ તરીકે, સમૂહમાંથી, જ્યાં સુપરસ્ક્રિપ્ટ પ્રકાર પરિમાણોની સંખ્યા સૂચવે છે. એચ. એમ. માં પ્રકાર કાર્યોનો સંપૂર્ણ સમૂહ મનસ્વી છે, સિવાય કે તેમાં ઓછામાં ઓછા, પ્રકારનાં કાર્યો હોવા જોઈએ. તે ઘણીવાર સુવિધા માટે ઇન્ફિક્સ નોટેશનમાં લખવામાં આવે છે. ઉદાહરણ તરીકે, સ્ટ્રિંગ્સ માટે પૂર્ણાંકોનું મેપિંગ કાર્યમાં પ્રકાર હોય છે. ફરીથી, કૌંસનો ઉપયોગ પ્રકાર અભિવ્યક્તિને અસ્પષ્ટ કરવા માટે થઈ શકે છે. એપ્લિકેશન ઇન્ફિક્સ તીર કરતાં વધુ મજબૂત રીતે જોડાય છે, જે જમણી-બંધનકર્તા છે. પ્રકાર ચલને મોનોટાઇપ્સ તરીકે સ્વીકારવામાં આવે છે. મોનોટાઇપ્સને મોનોમોર્ફિક પ્રકારો સાથે ભેળસેળ ન કરવી જોઈએ, જે ચલને બાકાત રાખે છે અને માત્ર પાયાની શરતોને મંજૂરી આપે છે. બે મોનોટાઇપ્સ સમાન હોય છે જો તેમની પાસે સમાન શરતો હોય. પોલીટાઇપ્સ પોલીટાઇપ્સ (અથવા પ્રકાર યોજનાઓ) એ એવા પ્રકારો છે જેમાં શૂન્ય અથવા વધુ માટે-બધા પરિમાણો દ્વારા બંધાયેલા ચલ હોય છે, દા. ત. . પોલીટાઇપ સાથેનું કાર્ય એક જ પ્રકારના કોઈપણ મૂલ્યને પોતાની સાથે મેપ કરી શકે છે, અને ઓળખ કાર્ય એ આ પ્રકાર માટેનું મૂલ્ય છે. બીજા ઉદાહરણ તરીકે, પૂર્ણાંકો માટે તમામ મર્યાદિત સમૂહોને મેપ કરતા કાર્યનો પ્રકાર છે. જે કાર્ય સમૂહની મુખ્યતાને પરત કરે છે તે આ પ્રકારનું મૂલ્ય હશે. ક્વોન્ટિફાયર માત્ર ટોચના સ્તર પર જ દેખાઈ શકે છે. દાખલા તરીકે, પ્રકારોને વાક્યરચના દ્વારા બાકાત રાખવામાં આવે છે. પોલીટાઇપ્સમાં મોનોટાઇપ્સનો પણ સમાવેશ થાય છે, આમ એક પ્રકારનું સામાન્ય સ્વરૂપ હોય છે, જ્યાં એક મોનોટાઇપ હોય છે. બહુપદીઓની સમાનતા એ પરિમાણને ફરીથી ગોઠવવા અને પરિમાણિત ચલોનું નામ બદલવા (-રૂપાંતર) પર આધારિત છે. વધુમાં, મોનોટાઇપમાં ન આવતા જથ્થાત્મક ચલને છોડી શકાય છે. સંદર્ભ અને ટાઇપિંગ હજી પણ અસંબદ્ધ ભાગો (વાક્યરચના અભિવ્યક્તિઓ અને પ્રકારો) ને અર્થપૂર્ણ રીતે એકસાથે લાવવા માટે ત્રીજો ભાગ જરૂરી છેઃ સંદર્ભ. વાક્યરચનામાં, સંદર્ભ એ જોડીની સૂચિ છે, જેને સોંપણીઓ, ધારણાઓ અથવા બંધન કહેવામાં આવે છે, દરેક જોડી જણાવે છે કે મૂલ્ય ચલનો પ્રકાર છે ત્રણેય ભાગો સંયુક્ત રીતે ફોર્મનો ટાઇપિંગ ચુકાદો આપે છે, જે દર્શાવે છે કે ધારણાઓ હેઠળ, અભિવ્યક્તિમાં પ્રકાર હોય છે. મુક્ત પ્રકારનાં ચલ એક પ્રકારમાં, પ્રતીક એ મોનોટાઇપમાં પ્રકારનાં ચલને બંધનકર્તા પરિમાણક છે. વેરિયેબલ્સને ક્વોન્ટિફાઇડ કહેવામાં આવે છે અને ક્વોન્ટિફાઇડ પ્રકારના વેરિયેબલની કોઈપણ ઘટનાને બાઉન્ડ કહેવામાં આવે છે અને તમામ અનબાઉન્ડ પ્રકારનાં વેરિયેબલ્સને ફ્રી કહેવામાં આવે છે. પોલીટાઇપ્સમાં માત્રાત્મકતા ઉપરાંત, પ્રકાર ચલ પણ સંદર્ભમાં બનવાથી બંધાયેલા હોઈ શકે છે, પરંતુ તેની જમણી બાજુએ ઊલટી અસર સાથે. આવા ચલ પછી ત્યાં પ્રકાર સ્થિરાંકોની જેમ વર્તે છે. છેવટે, ટાઇપ વેરિયેબલ કાયદેસર રીતે ટાઇપિંગમાં અનબાઉન્ડ થઈ શકે છે, જે કિસ્સામાં તેઓ ગર્ભિત રીતે બધા-પ્રમાણિત હોય છે. પ્રોગ્રામિંગ ભાષાઓમાં બાઉન્ડ અને અનબાઉન્ડ પ્રકારનાં ચલોની હાજરી થોડી અસામાન્ય છે. મોટેભાગે, તમામ પ્રકારના ચલને સંપૂર્ણ રીતે તમામ-માત્રામાં ગણવામાં આવે છે. દાખલા તરીકે, પ્રોલોગમાં મુક્ત ચલ સાથેની કલમો નથી. તેવી જ રીતે હાસ્કેલમાં, જ્યાં તમામ પ્રકારના ચલ પરોક્ષ રીતે માત્રાત્મક રીતે જોવા મળે છે, એટલે કે. હાસ્કેલ પ્રકાર a-> a નો અર્થ અહીં થાય છે. સોંપણીઓની જમણી બાજુની બંધનકર્તા અસર સંબંધિત અને ખૂબ જ અસામાન્ય છે. સામાન્ય રીતે, બાઉન્ડ અને અનબાઉન્ડ બંને પ્રકારના ચલોનું મિશ્રણ અભિવ્યક્તિમાં મુક્ત ચલોના ઉપયોગમાંથી ઉદ્ભવે છે. અચળ કાર્ય K = એક ઉદાહરણ પૂરું પાડે છે. તેમાં મોનોટાઇપ છે. કોઈ બહુરૂપતાને આના દ્વારા દબાણ કરી શકે છે. અહીં, પ્રકાર છે. મુક્ત મોનોટાઇપ ચલ આસપાસના અવકાશમાં બંધાયેલા ચલના પ્રકારમાંથી ઉદ્દભવે છે. પ્રકાર ધરાવે છે. કોઈ પણ મુક્ત પ્રકારનાં ચલની કલ્પના કરી શકે છે કે જે પ્રકાર દ્વારા બંધાયેલ છે. પરંતુ આવા અવકાશને એચ. એમ. માં વ્યક્ત કરી શકાતો નથી. તેના બદલે, બંધન સંદર્ભ દ્વારા સાકાર થાય છે. પ્રકાર ક્રમ બહુરૂપતાનો અર્થ એ છે કે એક અને સમાન અભિવ્યક્તિમાં (કદાચ અનંત) ઘણા પ્રકારો હોઈ શકે છે. પરંતુ આ પ્રકારની પ્રણાલીમાં, આ પ્રકારો સંપૂર્ણપણે અસંબંધિત નથી, પરંતુ પેરામેટ્રિક પોલીમોર્ફિઝમ દ્વારા આયોજિત છે. ઉદાહરણ તરીકે, ઓળખ તેના પ્રકાર તેમજ અથવા અને અન્ય ઘણા હોઈ શકે છે, પરંતુ નહીં. આ કાર્ય માટેનો સૌથી સામાન્ય પ્રકાર છે, જ્યારે અન્ય વધુ ચોક્કસ છે અને પ્રકાર પરિમાણ માટે અન્ય પ્રકારને સતત બદલીને સામાન્યમાંથી મેળવી શકાય છે, એટલે કે. પરિમાણિત ચલ. પ્રતિ-ઉદાહરણ નિષ્ફળ જાય છે કારણ કે રિપ્લેસમેન્ટ સુસંગત નથી. લેખિત પ્રકારની મુદતમાં અવેજી લાગુ કરીને સુસંગત બદલીને ઔપચારિક બનાવી શકાય છે. ઉદાહરણ સૂચવે છે તેમ, અવેજી માત્ર એક ક્રમ સાથે મજબૂત રીતે સંબંધિત નથી, જે વ્યક્ત કરે છે કે એક પ્રકાર વધુ કે ઓછો વિશેષ છે, પણ તમામ-પરિમાણ સાથે પણ જે અવેજીને લાગુ કરવાની મંજૂરી આપે છે. ઔપચારિક રીતે, એચ. એમ. માં, એક પ્રકાર વધુ સામાન્ય હોય છે, ઔપચારિક રીતે, જો કેટલાક પરિમાણિત ચલને સતત એવી રીતે બદલવામાં આવે કે જે બાજુની પટ્ટીમાં બતાવ્યા પ્રમાણે લાભ મેળવે. આ ક્રમ પ્રકાર પ્રણાલીની પ્રકાર વ્યાખ્યાનો એક ભાગ છે. અમારા અગાઉના ઉદાહરણમાં, અવેજી લાગુ કરવાથી પરિણામ મળશે. જ્યારે માત્રાત્મક ચલ માટે મોનોમોર્ફિક (ગ્રાઉન્ડ) પ્રકારને બદલવો એ સીધું આગળ છે, ત્યારે પોલીટાઇપને બદલવામાં મુક્ત ચલની હાજરીને કારણે કેટલાક મુશ્કેલીઓ છે. ખાસ કરીને, અનબાઉન્ડ વેરિયેબલ્સને બદલવા જોઈએ નહીં. તેમને અહીં સ્થિરાંક તરીકે ગણવામાં આવે છે. વધુમાં, પરિમાણો માત્ર ઉચ્ચ-સ્તર પર જ થઈ શકે છે. પેરામેટ્રિક પ્રકારને બદલીને, તેના પરિમાણોને ઉપાડવું પડે છે. જમણી બાજુનું ટેબલ નિયમને ચોક્કસ બનાવે છે. વૈકલ્પિક રીતે, ક્વોન્ટિફાયર્સ વિનાના બહુપદી માટે સમકક્ષ સંકેતને ધ્યાનમાં લો જેમાં ક્વોન્ટિફાઇડ વેરિયેબલ્સ પ્રતીકોના અલગ સમૂહ દ્વારા રજૂ થાય છે. આવા સંકેતલિપીમાં, વિશેષતા આવા ચલની સાદા સુસંગત બદલીમાં ઘટાડો કરે છે. સંબંધ એ આંશિક ક્રમ છે અને તેનું સૌથી નાનું તત્વ છે. મુખ્ય પ્રકાર જ્યારે પ્રકાર યોજનાની વિશેષતા એ ક્રમનો એક ઉપયોગ છે, તે પ્રકાર પ્રણાલીમાં નિર્ણાયક બીજી ભૂમિકા ભજવે છે. બહુરૂપીકરણ સાથેના પ્રકારનાં અનુમાનને અભિવ્યક્તિમાં હોઈ શકે તેવા તમામ સંભવિત પ્રકારોનો સારાંશ આપવાના પડકારનો સામનો કરવો પડે છે. ક્રમ બાંહેધરી આપે છે કે આવા સારાંશ અભિવ્યક્તિનો સૌથી સામાન્ય પ્રકાર તરીકે અસ્તિત્વ ધરાવે છે. ટાઇપિંગમાં અવેજી ઉપર વ્યાખ્યાયિત પ્રકાર ક્રમને ટાઇપિંગ સુધી વિસ્તૃત કરી શકાય છે કારણ કે ટાઇપિંગનું ગર્ભિત સર્વ-પરિમાણ સુસંગત પ્રતિસ્થાપનને સક્ષમ કરે છેઃ વિશેષતાના નિયમથી વિપરીત, આ વ્યાખ્યાનો ભાગ નથી, પરંતુ ગર્ભિત સર્વ-પરિમાણની જેમ આગળ વ્યાખ્યાયિત પ્રકાર નિયમોનું પરિણામ છે. ટાઇપિંગમાં મુક્ત પ્રકારનાં ચલ સંભવિત સુધારણા માટે પ્લેસહોલ્ડર તરીકે કામ કરે છે. તેની જમણી બાજુએ મુક્ત પ્રકારનાં ચલ માટે પર્યાવરણની બંધનકર્તા અસર વિશેષતાના નિયમમાં તેમના અવેજીને પ્રતિબંધિત કરે છે તે ફરીથી છે કે રિપ્લેસમેન્ટ સુસંગત હોવું જોઈએ અને તેમાં સંપૂર્ણ ટાઇપિંગનો સમાવેશ કરવાની જરૂર પડશે. આ લેખમાં ચાર જુદા જુદા નિયમ સમૂહોની ચર્ચા કરવામાં આવશેઃ ઘોષણાત્મક પ્રણાલી વાક્યરચના પ્રણાલી અલ્ગોરિધમ જે અલ્ગોરિધમ ડબલ્યુ ડિડક્ટિવ પ્રણાલી એચ. એમ. નું વાક્યરચના ઔપચારિક પ્રણાલીના મુખ્ય ભાગની રચના કરતા અનુમાન નિયમોના વાક્યરચના તરફ આગળ ધપાવવામાં આવે છે, જેમાં ટાઇપિંગનો નિર્ણય તરીકે ઉપયોગ કરવામાં આવે છે. દરેક નિયમ વ્યાખ્યાયિત કરે છે કે કયા પરિસરમાંથી કયા નિષ્કર્ષ પર આવી શકાય છે. ચુકાદાઓ ઉપરાંત, ઉપર રજૂ કરવામાં આવેલી કેટલીક વધારાની શરતોનો ઉપયોગ પરિસર તરીકે પણ થઈ શકે છે. નિયમોનો ઉપયોગ કરતો પુરાવો એ ચુકાદાઓનો ક્રમ છે જેમ કે નિષ્કર્ષ પહેલાં તમામ પરિસર સૂચિબદ્ધ હોય છે. નીચે આપેલા ઉદાહરણો પુરાવાઓનું સંભવિત સ્વરૂપ દર્શાવે છે. ડાબેથી જમણે, દરેક પંક્તિ નિષ્કર્ષ દર્શાવે છે, લાગુ કરાયેલ નિયમ અને પરિસર, કાં તો અગાઉની પંક્તિ (સંખ્યા) નો ઉલ્લેખ કરીને જો આધાર ચુકાદો હોય અથવા વિધેય સ્પષ્ટ કરીને. ટાઇપિંગના નિયમો પણ જુઓ ટાઇપિંગના નિયમો સાઇડ બોક્સ એચ. એમ. પ્રકારની સિસ્ટમના કપાતના નિયમો દર્શાવે છે. નિયમોને આશરે બે જૂથોમાં વહેંચી શકાય છેઃ પ્રથમ ચાર નિયમો (ચલ અથવા કાર્યની પહોંચ), (એપ્લિકેશન, એટલે કે. ફંક્શન કૉલ એક પરિમાણ સાથે), (અમૂર્તતા, એટલે કે. કાર્ય ઘોષણા) અને (ચલ ઘોષણા) વાક્યરચનાની આસપાસ કેન્દ્રિત છે, જે દરેક અભિવ્યક્તિ સ્વરૂપો માટે એક નિયમ રજૂ કરે છે. તેમનો અર્થ પ્રથમ નજરમાં સ્પષ્ટ છે, કારણ કે તેઓ દરેક અભિવ્યક્તિને વિઘટિત કરે છે, તેમની પેટા અભિવ્યક્તિઓ સાબિત કરે છે અને અંતે પરિસરમાં જોવા મળતા વ્યક્તિગત પ્રકારોને નિષ્કર્ષમાં પ્રકાર સાથે જોડે છે. બીજું જૂથ બાકીના બે નિયમો દ્વારા રચાય છે અને. તેઓ પ્રકારોની વિશેષતા અને સામાન્યીકરણનું સંચાલન કરે છે. જ્યારે ઉપરોક્ત વિશેષતા પરના વિભાગમાંથી નિયમ સ્પષ્ટ હોવો જોઈએ, ત્યારે વિરુદ્ધ દિશામાં કામ કરતા પહેલા વિભાગને પૂરક બનાવે છે. તે સામાન્યીકરણને મંજૂરી આપે છે, એટલે કે. સંદર્ભમાં બંધાયેલા ન હોય તેવા મોનોટાઇપ ચલોનું પ્રમાણ નક્કી કરવા માટે. નીચેના બે ઉદાહરણો નિયમ પ્રણાલીનો અમલ કરે છે. અભિવ્યક્તિ અને પ્રકાર બંને આપવામાં આવ્યાં હોવાથી, તે નિયમોનો પ્રકાર-તપાસનો ઉપયોગ છે. ઉદાહરણ તરીકેઃ ક્યાં લખી શકાય તેનો પુરાવોઃ સામાન્યીકરણ દર્શાવવા માટે, નીચે દર્શાવવામાં આવ્યું છેઃ ચાલો-બહુરૂપતા તરત જ દેખાતી નથી, નિયમ સમૂહ એવા નિયમનને એન્કોડ કરે છે કે જે સંજોગોમાં નિયમોમાં મોનો-અને પોલીટાઇપ્સના થોડો અલગ ઉપયોગ દ્વારા પ્રકારને સામાન્યીકૃત કરી શકાય છે અથવા નહીં. તે યાદ રાખો અને અનુક્રમે પોલી-અને મોનોટાઇપ્સને સૂચવો. નિયમમાં, કાર્યના પરિમાણનું મૂલ્ય ચલ આધાર દ્વારા મોનોમોર્ફિક પ્રકાર સાથે સંદર્ભમાં ઉમેરવામાં આવે છે, જ્યારે નિયમમાં, ચલ બહુરૂપી સ્વરૂપમાં પર્યાવરણમાં પ્રવેશ કરે છે. જો કે બંને કિસ્સાઓમાં સંદર્ભમાં ની હાજરી સોંપણીમાં કોઈપણ મુક્ત ચલ માટે સામાન્યીકરણ નિયમના ઉપયોગને અટકાવે છે, આ નિયમન-અભિવ્યક્તિમાં પરિમાણના પ્રકારને મોનોમોર્ફિક રહેવા માટે દબાણ કરે છે, જ્યારે અભિવ્યક્તિમાં, ચલને બહુપરીમાણીય રજૂ કરી શકાય છે, જેનાથી વિશેષતાઓ શક્ય બને છે. આ નિયમનના પરિણામે, ટાઇપ કરી શકાતું નથી, કારણ કે પરિમાણ મોનોમોર્ફિક સ્થિતિમાં હોય છે, જ્યારે પ્રકાર હોય છે, કારણ કે તેને લેટ-એક્સપ્રેશનમાં રજૂ કરવામાં આવ્યું છે અને તેથી તેને પોલીમોર્ફિક ગણવામાં આવે છે. સામાન્યીકરણનો નિયમ સામાન્યીકરણનો નિયમ પણ નજીકથી જોવા માટે યોગ્ય છે. અહીં, આધારમાં ગર્ભિત સર્વ-માત્રાને નિષ્કર્ષની જમણી બાજુએ ખસેડવામાં આવે છે. આ શક્ય છે, કારણ કે તે સંદર્ભમાં મુક્ત રીતે થતું નથી. ફરીથી, જ્યારે આ સામાન્યીકરણના નિયમને બુદ્ધિગમ્ય બનાવે છે, તે ખરેખર પરિણામ નથી. તેનાથી વિપરીત, સામાન્યીકરણનો નિયમ એ એચ. એમ. ની પ્રકાર પ્રણાલીની વ્યાખ્યાનો એક ભાગ છે અને ગર્ભિત સર્વ-માત્રાત્મક પરિણામ છે. એક અનુમાન અલ્ગોરિધમ હવે જ્યારે એચ. એમ. ની કપાત પ્રણાલી હાથમાં છે, ત્યારે કોઈ એક અલ્ગોરિધમ રજૂ કરી શકે છે અને નિયમોના સંદર્ભમાં તેને માન્ય કરી શકે છે. વૈકલ્પિક રીતે, નિયમો કેવી રીતે ક્રિયાપ્રતિક્રિયા કરે છે અને પુરાવા રચાય છે તેના પર નજીકથી નજર નાખીને તેને મેળવવું શક્ય બની શકે છે. આ આ લેખના બાકીના ભાગમાં ટાઇપિંગ સાબિત કરતી વખતે સંભવિત નિર્ણયો પર ધ્યાન કેન્દ્રિત કરીને કરવામાં આવે છે. નિયમો પસંદ કરવાની સ્વતંત્રતાની ડિગ્રી પુરાવાઓમાં બિંદુઓને અલગ કરીને, જ્યાં કોઈ નિર્ણય શક્ય નથી, વાક્યરચનાની આસપાસ કેન્દ્રિત નિયમોનું પ્રથમ જૂથ કોઈ વિકલ્પ છોડતું નથી કારણ કે દરેક વાક્યરચના નિયમ એક અનન્ય ટાઇપિંગ નિયમને અનુરૂપ હોય છે, જે સાબિતીનો એક ભાગ નક્કી કરે છે, જ્યારે નિષ્કર્ષ અને આ નિશ્ચિત ભાગોની સાંકળોના પરિસર વચ્ચે અને આવી શકે છે. આવી સાંકળ સાબિતીના નિષ્કર્ષ અને સર્વોચ્ચ અભિવ્યક્તિ માટેના નિયમ વચ્ચે પણ અસ્તિત્વમાં હોઈ શકે છે. તમામ પુરાવાઓ સ્કેચ કરેલા આકારના હોવા જોઈએ. કારણ કે નિયમ પસંદગીના સંદર્ભમાં સાબિતીમાં એકમાત્ર પસંદગી અને સાંકળો છે, સાબિતીનું સ્વરૂપ એ પ્રશ્ન સૂચવે છે કે શું તેને વધુ ચોક્કસ બનાવી શકાય છે, જ્યાં આ સાંકળોની જરૂર નથી. આ હકીકતમાં શક્ય છે અને આવા કોઈ નિયમો વિના નિયમો પ્રણાલીના એક પ્રકાર તરફ દોરી જાય છે. વાક્યરચના-નિર્દેશિત નિયમ પ્રણાલી એચ. એમ. ની સમકાલીન સારવાર મધ્યવર્તી પગલા તરીકે ક્લેમેન્ટને કારણે શુદ્ધ વાક્યરચના-નિર્દેશિત નિયમ પ્રણાલીનો ઉપયોગ કરે છે. આ પ્રણાલીમાં, વિશેષતા મૂળ નિયમ પછી સીધી સ્થિત થાય છે અને તેમાં ભળી જાય છે, જ્યારે સામાન્યીકરણ નિયમનો ભાગ બની જાય છે. ત્યાં સામાન્યીકરણ પણ કાર્યની રજૂઆત કરીને હંમેશા સૌથી સામાન્ય પ્રકારનું ઉત્પાદન કરવા માટે નક્કી કરવામાં આવે છે, જે બંધાયેલા ન હોય તેવા તમામ મોનોટાઇપ ચલોનું પ્રમાણ નક્કી કરે છે. ઔપચારિક રીતે, આ નવી નિયમ પ્રણાલી મૂળની સમકક્ષ છે તે માન્ય કરવા માટે, વ્યક્તિએ તે બતાવવું પડશે, જે બે પેટા-પુરાવાઓમાં વિઘટિત થાય છેઃ (સુસંગતતા) (પૂર્ણતા) જ્યારે સુસંગતતા નિયમોને વિઘટિત કરીને અને પુરાવામાં જોઈ શકાય છે, તે સંભવતઃ અપૂર્ણ દેખાય છે, જેમ કે કોઈ વ્યક્તિ બતાવી શકતું નથી, પરંતુ માત્ર. સંપૂર્ણતાનું માત્ર થોડું નબળું સંસ્કરણ સાબિત કરી શકાય તેવું છે, એટલે કે, અંતે સાબિતીને સામાન્ય બનાવવાની મંજૂરી આપતા અભિવ્યક્તિ માટે મુખ્ય પ્રકાર મેળવી શકાય છે. સરખામણી અને, હવે તમામ નિયમોના ચુકાદાઓમાં માત્ર મોનોટાઇપ્સ દેખાય છે. વધુમાં, કપાત પદ્ધતિ સાથેના કોઈપણ સંભવિત સાબિતીનો આકાર હવે અભિવ્યક્તિનો આકાર (બંને વૃક્ષો તરીકે જોવામાં આવે છે) સમાન છે. આમ અભિવ્યક્તિ સાબિતીનો આકાર સંપૂર્ણપણે નક્કી કરે છે. આકારમાં સંભવતઃ અને સિવાયના તમામ નિયમોના સંદર્ભમાં નક્કી કરવામાં આવશે, જે અન્ય ગાંઠો વચ્ચે મનસ્વી રીતે લાંબી શાખાઓ (સાંકળો) બનાવવાની મંજૂરી આપે છે. ડિગ્રીઝ ઓફ ફ્રીડમ નિયમોને ત્વરિત બનાવે છે હવે જ્યારે સાબિતીનો આકાર જાણી શકાય છે, ત્યારે તે પહેલાથી જ એક પ્રકારનો અનુમાન અલ્ગોરિધમ તૈયાર કરવાની નજીક છે. કારણ કે આપેલ અભિવ્યક્તિ માટેના કોઈપણ સાબિતીનો આકાર સમાન હોવો જોઈએ, તેથી સાબિતીના ચુકાદાઓમાં મોનોટાઇપ્સને અનિશ્ચિત હોવાનું માની શકાય છે અને તેમને કેવી રીતે નક્કી કરવું તે અંગે વિચારણા કરી શકાય છે. અહીં, અવેજી (વિશેષતા) ક્રમ અમલમાં આવે છે. જો કે પ્રથમ નજરમાં કોઈ સ્થાનિક રીતે પ્રકારો નક્કી કરી શકતું નથી, તેમ છતાં આશા છે કે પ્રૂફ ટ્રીને પસાર કરતી વખતે ક્રમની મદદથી તેમને સુધારવું શક્ય છે, વધુમાં એમ ધારીને કે પરિણામી અલ્ગોરિધમ એક અનુમાન પદ્ધતિ બનવાનું છે, કે કોઈપણ આધારમાં પ્રકાર શક્ય તેટલો શ્રેષ્ઠ તરીકે નક્કી કરવામાં આવશે. અને હકીકતમાં, સૂચનોના નિયમો પર નજર કરીએ તોઃ નિર્ણાયક પસંદગી છે. આ તબક્કે, તેના વિશે કંઇ જાણીતું નથી, તેથી કોઈ ફક્ત સૌથી સામાન્ય પ્રકાર ધારણ કરી શકે છે, જે છે. જો તે જરૂરી બને તો તે પ્રકારને વિશેષતા આપવાની યોજના છે. કમનસીબે, આ જગ્યાએ પોલીટાઇપ કરવાની મંજૂરી નથી, તેથી કેટલાકને આ ક્ષણે કરવું પડે છે. અનિચ્છનીય કેપ્ચર્સને ટાળવા માટે, સાબિતીમાં હજુ સુધી ન હોય તેવો પ્રકાર ચલ એ સલામત પસંદગી છે. વધુમાં, કોઈએ ધ્યાનમાં રાખવું પડશે કે આ મોનોટાઇપ હજી નિશ્ચિત નથી, પરંતુ તેને વધુ શુદ્ધ કરી શકાય છે. : પસંદગી એ છે કે કેવી રીતે શુદ્ધ કરવું. કારણ કે અહીં કોઈ પણ પ્રકારની પસંદગી વેરિયેબલના ઉપયોગ પર આધારિત છે, જે સ્થાનિક રીતે જાણીતું નથી, સૌથી સુરક્ષિત શરત સૌથી સામાન્ય છે. ઉપરની સમાન પદ્ધતિનો ઉપયોગ કરીને બધા માત્રાત્મક ચલને નવા મોનોટાઇપ ચલ સાથે ત્વરિત કરી શકાય છે, ફરીથી તેમને વધુ શુદ્ધિકરણ માટે ખુલ્લા રાખી શકાય છે. : નિયમ કોઈ વિકલ્પ છોડતો નથી. કરી નાંખ્યું. : માત્ર એપ્લિકેશન નિયમ બંને પરિસર દ્વારા જરૂરી હોય તેટલા અત્યાર સુધી "ખોલેલા" ચલ માટે શુદ્ધિકરણ માટે દબાણ કરી શકે છે. પ્રથમ આધાર અનુમાનના પરિણામને સ્વરૂપમાં હોવાનું દબાણ કરે છે. જો એમ હોય તો ઠીક છે. પછીથી પરિણામ માટે તેને પસંદ કરી શકાય છે. જો નહીં, તો તે એક ઓપન વેરિયેબલ હોઈ શકે છે. પછી આને પહેલાની જેમ બે નવા ચલ સાથે જરૂરી સ્વરૂપમાં શુદ્ધ કરી શકાય છે. નહિંતર, પ્રકાર તપાસ નિષ્ફળ જાય છે કારણ કે પ્રથમ આધાર એક પ્રકારનું અનુમાન કરે છે જે કાર્ય પ્રકારમાં નથી અને બનાવી શકાતો નથી. બીજા આધાર માટે જરૂરી છે કે અનુમાનિત પ્રકાર પ્રથમ આધારની બરાબર હોય. હવે બે સંભવિત રીતે જુદા જુદા પ્રકારો છે, કદાચ ખુલ્લા પ્રકારનાં ચલ સાથે, સરખામણી કરવા માટે અને જો શક્ય હોય તો સમાન બનાવવા માટે. જો તે હોય, તો શુદ્ધિકરણ જોવા મળે છે, અને જો નહીં, તો ફરીથી એક પ્રકારની ભૂલ મળી આવે છે. એક અસરકારક પદ્ધતિ અવેજી દ્વારા "બે શબ્દોને સમાન બનાવવા" માટે જાણીતી છે, કહેવાતા યુનિયન-ફાઇન્ડ અલ્ગોરિધમ સાથે સંયોજનમાં રોબિન્સનનું એકીકરણ. યુનિયન-ફાઇન્ડ અલ્ગોરિધમનો ટૂંકમાં સારાંશ આપવા માટે, સાબિતીમાં તમામ પ્રકારોના સમૂહને જોતાં, તે પ્રક્રિયાના માધ્યમથી તેમને સમાનતા વર્ગોમાં એકસાથે જૂથબદ્ધ કરવાની અને પ્રક્રિયાનો ઉપયોગ કરીને આવા દરેક વર્ગ માટે પ્રતિનિધિ પસંદ કરવાની મંજૂરી આપે છે. આડઅસરના અર્થમાં પ્રક્રિયા શબ્દ પર ભાર મૂકતા, અમે અસરકારક અલ્ગોરિધમ તૈયાર કરવા માટે સ્પષ્ટ રીતે તર્કનું ક્ષેત્ર છોડી રહ્યા છીએ. a નો પ્રતિનિધિ એવી રીતે નક્કી કરવામાં આવે છે કે, જો બંને અને પ્રકાર ચલ હોય તો પ્રતિનિધિ આપખુદ રીતે તેમાંથી એક હોય છે, પરંતુ ચલ અને પદને એકીકૃત કરતી વખતે, શબ્દ પ્રતિનિધિ બની જાય છે. હાથમાં યુનિયન-ફાઇન્ડના અમલીકરણને ધારીએ તો, બે મોનોટાઇપ્સનું એકીકરણ નીચે પ્રમાણે કરી શકાય છેઃ એકીકૃત કરો (ta, tb): ta = શોધો (ta) tb = શોધો (tb) જો બંને ta, tb સમાન D, n સાથે ફોર્મ D p1.pn ની શરતો હોય તો પછી દરેક અનુરૂપ ith પરિમાણ માટે એકીકૃત કરો (ta [i], tb [i]) અન્યથા જો ઓછામાં ઓછું એક ta, tb એક પ્રકારનો ચલ હોય તો યુનિયન (ta, tb) અન્યથા ભૂલ 'પ્રકારો મેળ ખાતા નથી' હવે હાથમાં અનુમાન અલ્ગોરિધમનો સ્કેચ હોય તો, આગામી વિભાગમાં વધુ ઔપચારિક પ્રસ્તુતિ આપવામાં આવે છે. તેનું વર્ણન મિલ્નર પી. 370 એફએફમાં કરવામાં આવ્યું છે. અલ્ગોરિધમ જે. અલ્ગોરિધમ જે. ની રજૂઆત એ તાર્કિક નિયમોના સંકેતનો દુરુપયોગ છે, કારણ કે તેમાં આડઅસરોનો સમાવેશ થાય છે પરંતુ તે જ સમયે કાર્યક્ષમ અમલીકરણને વ્યક્ત કરતી વખતે તેની સાથે સીધી સરખામણી કરવાની મંજૂરી આપે છે. નિયમો હવે એવા પરિમાણો સાથેની પ્રક્રિયાને સ્પષ્ટ કરે છે જે નિષ્કર્ષમાં પરિણમે છે કે જ્યાં પરિસરનો અમલ ડાબેથી જમણે થાય છે. આ પ્રક્રિયા શબ્દની નકલ કરીને અને બાઉન્ડ પ્રકારનાં ચલને સતત નવા મોનોટાઇપ ચલ દ્વારા બદલીને પોલીટાઇપમાં વિશેષતા ધરાવે છે. નવી મોનોટાઇપ ચલ પેદા કરે છે. સંભવતઃ, અનિચ્છનીય કેપ્ચર ટાળવા માટે ક્વોન્ટિફિકેશન માટે નવા વેરિયેબલ્સ રજૂ કરતા પ્રકારની નકલ કરવી પડશે. એકંદરે, એલ્ગોરિધમ હવે હંમેશા એકીકરણ માટે વિશેષતાને છોડીને સૌથી સામાન્ય પસંદગી કરીને આગળ વધે છે, જે પોતે જ સૌથી સામાન્ય પરિણામ ઉત્પન્ન કરે છે. ઉપર નોંધ્યા મુજબ, આપેલ અભિવ્યક્તિ માટે સૌથી સામાન્ય પ્રકાર મેળવવા માટે, અંતિમ પરિણામને અંતે સામાન્ય બનાવવું પડશે. કારણ કે અલ્ગોરિધમમાં ઉપયોગમાં લેવાતી પ્રક્રિયાઓ લગભગ ઓ (1) ખર્ચ ધરાવે છે, અલ્ગોરિધમનો એકંદર ખર્ચ અભિવ્યક્તિના કદમાં રેખીયની નજીક છે, જેના માટે એક પ્રકારનું અનુમાન લગાવવાનું છે. આ પ્રકાર અનુમાન અલ્ગોરિધમ્સ મેળવવાના અન્ય ઘણા પ્રયાસોથી વિપરીત છે, જે ઘણીવાર એન. પી.-હાર્ડ હોવાનું બહાર આવ્યું છે, જો સમાપ્તિના સંદર્ભમાં અનિશ્ચિત ન હોય તો. આમ એચ. એમ. પ્રદર્શન કરે છે તેમજ શ્રેષ્ઠ સંપૂર્ણ રીતે માહિતગાર પ્રકાર-તપાસ અલ્ગોરિધમ્સ કરી શકે છે. અહીં ટાઇપ-ચેકિંગનો અર્થ એ છે કે અલ્ગોરિધમને સાબિતી શોધવાની જરૂર નથી, પરંતુ માત્ર આપેલાને માન્ય કરવા માટે. કાર્યક્ષમતામાં થોડો ઘટાડો થાય છે કારણ કે સંદર્ભમાં પ્રકાર ચલોનું બંધન જાળવવું પડે છે જેથી ગણતરીની મંજૂરી મળે અને તે દરમિયાન પુનરાવર્તિત પ્રકારોના નિર્માણને રોકવા માટે તપાસ થાય. આવા કેસનું ઉદાહરણ છે, જેના માટે એચ. એમ. નો ઉપયોગ કરીને કોઈ પ્રકાર મેળવી શકાતો નથી. વ્યવહારીક રીતે, પ્રકારો માત્ર નાના શબ્દો છે અને વિસ્તરણ માળખાઓનું નિર્માણ કરતા નથી. આમ, જટિલતા વિશ્લેષણમાં, તેમની સરખામણીને સતત, ઓ (1) ખર્ચ જાળવી રાખવા તરીકે ગણી શકાય. અલ્ગોરિધમનો પુરાવો અગાઉના વિભાગમાં, અલ્ગોરિધમનો સ્કેચ કરતી વખતે તેના સાબિતીને ધાતુશાસ્ત્રીય દલીલ સાથે સંકેત આપવામાં આવ્યો હતો. જ્યારે આ એક કાર્યક્ષમ અલ્ગોરિધમ J તરફ દોરી જાય છે, તે સ્પષ્ટ નથી કે શું અલ્ગોરિધમ ડિડક્શન સિસ્ટમ્સ D અથવા S ને યોગ્ય રીતે પ્રતિબિંબિત કરે છે કે જે સિમેન્ટીક બેઝ લાઇન તરીકે કામ કરે છે. ઉપરોક્ત દલીલમાં સૌથી નિર્ણાયક મુદ્દો એ સંદર્ભ દ્વારા બંધાયેલા મોનોટાઇપ ચલોનું શુદ્ધિકરણ છે. દાખલા તરીકે, અલ્ગોરિધમ હિંમતભેર સંદર્ભમાં ફેરફાર કરે છે જ્યારે ઉદાહરણ તરીકે. , કારણ કે પરિમાણના સંદર્ભમાં ઉમેરવામાં આવેલા મોનોટાઇપ ચલને પછીથી એપ્લિકેશનને સંભાળતી વખતે શુદ્ધ કરવાની જરૂર છે. સમસ્યા એ છે કે કપાતના નિયમો આવા શુદ્ધિકરણની મંજૂરી આપતા નથી. એવી દલીલ કરવી કે શુદ્ધ પ્રકારને મોનોટાઇપ ચલને બદલે અગાઉ ઉમેરી શકાયો હોત તે શ્રેષ્ઠ રીતે અનુકૂળ છે. ઔપચારિક રીતે સંતોષકારક દલીલ સુધી પહોંચવાની ચાવી એ છે કે સંદર્ભને શુદ્ધિકરણમાં યોગ્ય રીતે સામેલ કરવો. ઔપચારિક રીતે, ટાઇપિંગ મુક્ત પ્રકારનાં ચલોનાં અવેજી સાથે સુસંગત છે. ફ્રી વેરિયેબલ્સને રિફાઇન કરવાનો અર્થ એ છે કે સમગ્ર ટાઇપિંગને રિફાઇન કરવું. એલ્ગોરિધમ W ત્યાંથી, અલ્ગોરિધમ J નો પુરાવો અલ્ગોરિધમ W તરફ દોરી જાય છે, જે ફક્ત અવેજી દ્વારા તેની ક્રમિક રચનાને વ્યક્ત કરીને પ્રક્રિયા દ્વારા લાદવામાં આવેલી આડઅસરોને સ્પષ્ટ કરે છે. સાઇડબારમાં અલ્ગોરિધમ W ની રજૂઆત હજુ પણ ઇટાલિકમાં સેટ કરેલી કામગીરીમાં આડઅસરોનો ઉપયોગ કરે છે, પરંતુ આ હવે નવા પ્રતીકો બનાવવા સુધી મર્યાદિત છે. ચુકાદાનું સ્વરૂપ એ છે કે, સંદર્ભ અને અભિવ્યક્તિ સાથેના કાર્યને વિકલ્પ સાથે મોનોટાઇપ ઉત્પન્ન કરતા પરિમાણ તરીકે સૂચવે છે. અવેજી ઉત્પન્ન કરવાની આડઅસર મુક્ત આવૃત્તિ છે જે સૌથી સામાન્ય એકીકરણકર્તા છે. જ્યારે અલ્ગોરિધમ W ને સામાન્ય રીતે HM અલ્ગોરિધમ માનવામાં આવે છે અને ઘણીવાર સાહિત્યમાં નિયમ પ્રણાલી પછી સીધી રીતે રજૂ કરવામાં આવે છે, ત્યારે તેનો હેતુ મિલ્નર દ્વારા પી. 369 પર નીચે મુજબ વર્ણવવામાં આવ્યો છેઃ જેમ તે ઊભું છે તેમ, W ભાગ્યે જ એક કાર્યક્ષમ અલ્ગોરિધમ છે; અવેજી ઘણી વાર લાગુ કરવામાં આવે છે. તે સ્વસ્થતાના સાબિતીને મદદ કરવા માટે ઘડવામાં આવ્યું હતું. હવે આપણે એક સરળ અલ્ગોરિધમ J રજૂ કરીએ છીએ જે ચોક્કસ અર્થમાં W નું અનુકરણ કરે છે. જ્યારે તેઓ W ને વધુ જટિલ અને ઓછા કાર્યક્ષમ માનતા હતા, ત્યારે તેમણે તેને જે. જે. સમક્ષ તેમના પ્રકાશનમાં રજૂ કર્યું હતું. જ્યારે આડઅસરો ઉપલબ્ધ ન હોય અથવા અનિચ્છનીય હોય ત્યારે તેના ફાયદા છે. W એ સંપૂર્ણતા સાબિત કરવા માટે પણ જરૂરી છે, જે તેના દ્વારા સાઉન્ડનેસ પ્રૂફમાં પરિબળ છે. સાબિતીની જવાબદારીઓ સાબિતીની જવાબદારીઓ ઘડતા પહેલા, નિયમો સિસ્ટમ ડી અને એસ અને પ્રસ્તુત અલ્ગોરિધમ્સ વચ્ચેના વિચલન પર ભાર મૂકવાની જરૂર છે. જ્યારે ઉપરના વિકાસમાં "ઓપન" પ્રૂફ વેરિયેબલ્સ તરીકે મોનોટાઇપ્સનો દુરુપયોગ કરવામાં આવ્યો હતો, ત્યારે યોગ્ય મોનોટાઇપ વેરિયેબલ્સને નુકસાન થવાની સંભાવનાને નવા વેરિયેબલ્સ રજૂ કરીને અને શ્રેષ્ઠની આશા રાખીને દૂર કરવામાં આવી હતી. પરંતુ એક કેચ છેઃ કરવામાં આવેલા વચનોમાંથી એક એ હતું કે આ નવા ચલોને "ધ્યાનમાં રાખવામાં આવશે". આ વચન અલ્ગોરિધમ દ્વારા પૂર્ણ થતું નથી. સંદર્ભ હોવાને કારણે, અભિવ્યક્તિને ક્યાંય અથવા ટાઇપ કરી શકાતી નથી, પરંતુ અલ્ગોરિધમ્સ પ્રકાર સાથે આવે છે, જ્યાં W વધુમાં અવેજી પહોંચાડે છે, એટલે કે અલ્ગોરિધમ તમામ પ્રકારની ભૂલોને શોધવામાં નિષ્ફળ જાય છે. પ્રૂફ વેરિયેબલ્સ અને મોનોટાઇપ વેરિયેબલ્સમાં વધુ કાળજીપૂર્વક તફાવત કરીને આ અવગણનાને સરળતાથી સુધારી શકાય છે. લેખકો આ સમસ્યાથી સારી રીતે વાકેફ હતા પરંતુ તેમણે તેને ઠીક ન કરવાનું નક્કી કર્યું. આની પાછળ કોઈ વ્યવહારિક કારણ હોઈ શકે છે. જ્યારે પ્રકાર અનુમાનને વધુ યોગ્ય રીતે અમલમાં મૂકવાથી એલ્ગોરિધમ એબ્સ્ટ્રેક્ટ મોનોટાઇપ્સ સાથે વ્યવહાર કરવા માટે સક્ષમ બન્યું હોત, ત્યારે તે ઇચ્છિત એપ્લિકેશન માટે જરૂરી ન હતું જ્યાં અગાઉથી અસ્તિત્વમાં રહેલા સંદર્ભમાં કોઈ પણ વસ્તુ મુક્ત ચલ ધરાવતી ન હોય. આ પ્રકાશમાં, બિનજરૂરી ગૂંચવણને સરળ અલ્ગોરિધમની તરફેણમાં છોડી દેવામાં આવી હતી. બાકીની નકારાત્મકતા એ છે કે નિયમ પ્રણાલીના સંદર્ભમાં અલ્ગોરિધમનો પુરાવો ઓછો સામાન્ય છે અને માત્ર એક આડઅસર તરીકે સંદર્ભો માટે જ બનાવી શકાય છે. સંપૂર્ણતાની જવાબદારીમાં બાજુની શરત સૂચવે છે કે કપાત કેવી રીતે ઘણા પ્રકારો આપી શકે છે, જ્યારે અલ્ગોરિધમ હંમેશા એક ઉત્પન્ન કરે છે. તે જ સમયે, બાજુની સ્થિતિ એવી માંગ કરે છે કે અનુમાનિત પ્રકાર ખરેખર સૌથી સામાન્ય છે. જવાબદારીઓને યોગ્ય રીતે સાબિત કરવા માટે પહેલા તેમને મજબૂત કરવાની જરૂર છે જેથી અને દ્વારા અવેજી થ્રેડિંગ અવેજી લેમ્માને સક્રિય કરવાની મંજૂરી મળે. ત્યાંથી, પુરાવાઓ અભિવ્યક્તિ પર ઇન્ડક્શન દ્વારા હોય છે. અન્ય સાબિતી જવાબદારી એ અવેજી લેમ્મા પોતે છે, એટલે કે. ટાઇપિંગની અવેજી, જે આખરે ઓલ-ક્વાન્ટિફિકેશન સ્થાપિત કરે છે. પછીનું ઔપચારિક રીતે સાબિત કરી શકાતું નથી, કારણ કે આવી કોઈ વાક્યરચના હાથમાં નથી. વિસ્તરણ પુનરાવર્તિત વ્યાખ્યાઓ પ્રોગ્રામિંગને વ્યવહારુ પુનરાવર્તિત કાર્યો બનાવવા માટે જરૂરી છે. લેમ્બડા કલનનો કેન્દ્રિય ગુણધર્મ એ છે કે પુનરાવર્તિત વ્યાખ્યાઓ સીધી ઉપલબ્ધ નથી, પરંતુ તેના બદલે નિશ્ચિત બિંદુ સંયોજક સાથે વ્યક્ત કરી શકાય છે. પરંતુ કમનસીબે, નીચે દર્શાવેલ સિસ્ટમ પર વિનાશક અસર કર્યા વિના ફિક્સપોઇન્ટ સંયોજકને લેમ્બડા કલનની ટાઇપ કરેલી આવૃત્તિમાં ઘડી શકાતું નથી. ટાઇપિંગ નિયમ મૂળ પેપર દર્શાવે છે કે પુનરાવર્તન સંયોજક દ્વારા અનુભવી શકાય છે. આમ સંભવિત પુનરાવર્તિત વ્યાખ્યાને આ રીતે ઘડી શકાય છે. વૈકલ્પિક રીતે અભિવ્યક્તિ વાક્યરચનાનું વિસ્તરણ અને વધારાના ટાઇપિંગ નિયમ શક્ય છેઃ જ્યાં મૂળભૂત રીતે મર્જ થાય છે અને મોનોટાઇપ સ્થિતિઓમાં પુનરાવર્તિત રીતે વ્યાખ્યાયિત ચલોનો સમાવેશ કરતી વખતે જ્યાં તેઓ ડાબી બાજુએ થાય છે પરંતુ તેની જમણી બાજુએ બહુપદી તરીકે. પરિણામો જ્યારે ઉપરોક્ત સીધી વાત છે, તે કિંમત પર આવે છે. પ્રકાર સિદ્ધાંત લેમ્બડા કલનને ગણતરી અને તર્ક સાથે જોડે છે. ઉપરોક્ત સરળ ફેરફાર બંને પર અસર કરે છેઃ મજબૂત સામાન્યીકરણ ગુણધર્મ અમાન્ય છે, કારણ કે બિન-સમાપ્તિ શરતો ઘડી શકાય છે. તર્ક તૂટી જાય છે કારણ કે પ્રકાર વસવાટ કરે છે. ઓવરલોડિંગનો અર્થ એ છે કે વિવિધ કાર્યોને એક જ નામથી વ્યાખ્યાયિત કરી શકાય છે અને તેનો ઉપયોગ કરી શકાય છે. મોટાભાગની પ્રોગ્રામિંગ ભાષાઓ ઓછામાં ઓછી બિલ્ટ-ઇન અંકગણિત કામગીરી (+, <, વગેરે) સાથે ઓવરલોડિંગ પ્રદાન કરે છે. ), પ્રોગ્રામરને સમાન સ્વરૂપમાં અંકગણિત અભિવ્યક્તિઓ લખવાની મંજૂરી આપવા માટે, ઇન્ટી અથવા વાસ્તવિક જેવા વિવિધ આંકડાકીય પ્રકારો માટે પણ. કારણ કે સમાન અભિવ્યક્તિમાં આ વિવિધ પ્રકારોનું મિશ્રણ પણ ગર્ભિત રૂપાંતરની માંગ કરે છે, ખાસ કરીને આ કામગીરીઓ માટે ઓવરલોડિંગ ઘણીવાર પ્રોગ્રામિંગ ભાષામાં જ બનાવવામાં આવે છે. કેટલીક ભાષાઓમાં, આ સુવિધાને સામાન્યીકૃત કરવામાં આવે છે અને વપરાશકર્તા માટે ઉપલબ્ધ કરાવવામાં આવે છે, દા. ત. સી + + માં. જ્યારે પ્રકાર તપાસ અને અનુમાન બંનેમાં ગણતરી ખર્ચ માટે કાર્યાત્મક પ્રોગ્રામિંગમાં કામચલાઉ ઓવરલોડિંગ ટાળવામાં આવ્યું છે, ત્યારે ઓવરલોડિંગને વ્યવસ્થિત કરવાની એક રીત રજૂ કરવામાં આવી છે જે ફોર્મ અને નામકરણ બંનેમાં ઓબ્જેક્ટ ઓરિએન્ટેડ પ્રોગ્રામિંગ સાથે મેળ ખાય છે, પરંતુ એક સ્તર ઉપરની તરફ કામ કરે છે. આ વ્યવસ્થિતમાં "ઉદાહરણો" પદાર્થો નથી (એટલે કે. મૂલ્ય સ્તર પર), પરંતુ તેના બદલે પ્રકારો. પરિચયમાં ઉલ્લેખિત ક્વિકસોર્ટ ઉદાહરણ ઓર્ડરમાં ઓવરલોડિંગનો ઉપયોગ કરે છે, જેમાં હાસ્કેલમાં નીચેની પ્રકારની ટિપ્પણી હોય છેઃ ક્વિકસોર્ટઃઃ ઓર્ડ a => [a]-> [a] અહીં, પ્રકાર a માત્ર બહુરૂપી નથી, પરંતુ અમુક પ્રકારનાં વર્ગ ઓર્ડના ઉદાહરણ તરીકે પણ પ્રતિબંધિત છે, જે વિધેયોના મુખ્ય ભાગમાં ઉપયોગમાં લેવાતા ક્રમમાં આગાહીઓ <અને> = પ્રદાન કરે છે. આ આગાહીઓના યોગ્ય અમલીકરણ પછી વધારાના પરિમાણો તરીકે ક્વિકસોર્ટને પસાર કરવામાં આવે છે, જલદી જ વધુ કોંક્રિટ પ્રકારો પર ક્વિકસોર્ટનો ઉપયોગ કરવામાં આવે છે જે ઓવરલોડેડ ફંક્શન ક્વિકસોર્ટનું એક જ અમલીકરણ પ્રદાન કરે છે. કારણ કે "વર્ગો" તેમની દલીલ તરીકે માત્ર એક જ પ્રકારને મંજૂરી આપે છે, પરિણામી પ્રકાર પ્રણાલી હજી પણ અનુમાન પ્રદાન કરી શકે છે. વધુમાં, પ્રકાર વર્ગો પછી અમુક પ્રકારના ઓવરલોડિંગ ઓર્ડરથી સજ્જ થઈ શકે છે જે વર્ગોને જાળી તરીકે ગોઠવવાની મંજૂરી આપે છે. ઉચ્ચ ક્રમના પ્રકારો પેરામેટ્રિક પોલીમોર્ફિઝમ સૂચવે છે કે પ્રકારો પોતાને પરિમાણો તરીકે પસાર કરવામાં આવે છે જાણે કે તેઓ યોગ્ય મૂલ્યો હોય. યોગ્ય કાર્યો માટે દલીલો તરીકે પસાર થાય છે, પરંતુ "પેરામેટ્રિક" પ્રકાર સ્થિરાંકોની જેમ "પ્રકાર કાર્યો" માં પણ પસાર થાય છે, તે પ્રશ્ન તરફ દોરી જાય છે કે પ્રકારો પોતાને વધુ યોગ્ય રીતે કેવી રીતે ટાઇપ કરવા. ઉચ્ચ ક્રમના પ્રકારોનો ઉપયોગ વધુ અભિવ્યક્ત પ્રકારની પ્રણાલી બનાવવા માટે થાય છે. કમનસીબે, મેટા પ્રકારોની હાજરીમાં એકીકરણ હવે નિર્ણાયક રહ્યું નથી, જે સામાન્યતાના આ વિસ્તરણમાં પ્રકાર અનુમાનને અશક્ય બનાવે છે. વધુમાં, બધા સમૂહોના સમૂહની જેમ, પ્રકાર તરીકે પોતાને સમાવતા તમામ પ્રકારોનો એક પ્રકાર વિરોધાભાસ તરફ દોરી જાય છે, તેથી વ્યક્તિએ અમૂર્તતાના સ્તરોના પગલાંઓમાં આગળ વધવું જોઈએ. સેકન્ડ ઓર્ડર લેમ્બડા કેલ્ક્યુલસમાં સંશોધન, એક પગલું ઉપરની તરફ, દર્શાવે છે કે આ સામાન્યતામાં પ્રકારનો અનુમાન અનિશ્ચિત છે. એક વધારાના સ્તરના ભાગોને હાસ્કેલ નામના પ્રકારમાં રજૂ કરવામાં આવ્યા છે, જ્યાં તેનો ઉપયોગ મોનાડ ટાઇપ કરવામાં મદદ કરવા માટે થાય છે. વિસ્તૃત પ્રકારની પ્રણાલીના આંતરિક મિકેનિક્સમાં પડદા પાછળ કામ કરતા પ્રકારોને ગર્ભિત છોડી દેવામાં આવે છે. સબટાઇપિંગ સબટાઇપિંગ અને પ્રકાર અનુમાનને જોડવાના પ્રયાસોથી થોડી નિરાશા થઈ છે. પેટા પ્રકારનાં અવરોધોને એકઠા કરવા અને તેનો પ્રચાર કરવો સરળ છે (પ્રકાર સમાનતાના અવરોધોથી વિપરીત), પરિણામી અવરોધોને અનુમાનિત ટાઇપિંગ યોજનાઓનો ભાગ બનાવે છે, ઉદાહરણ તરીકે, જ્યાં પ્રકાર ચલ પર અવરોધ છે. જો કે, કારણ કે પ્રકાર ચલ હવે આ અભિગમમાં આતુરતાથી એકીકૃત નથી, તે ઘણી નકામી પ્રકાર ચલ અને અવરોધો ધરાવતી મોટી અને વિશાળ ટાઇપિંગ યોજનાઓ પેદા કરે છે, જેનાથી તેમને વાંચવું અને સમજવું મુશ્કેલ બને છે. તેથી, બિનનિર્ધારણીય મર્યાદિત ઓટોમેટન (એન. એફ. એ.) સરળીકરણ (અનુમાનિત પુનરાવર્તિત પ્રકારોની હાજરીમાં ઉપયોગી) જેવી તકનીકોનો ઉપયોગ કરીને, આવી ટાઇપિંગ યોજનાઓ અને તેમની મર્યાદાઓને સરળ બનાવવા માટે નોંધપાત્ર પ્રયાસો કરવામાં આવ્યા હતા. તાજેતરમાં, ડોલન અને માયક્રોફ્ટે ટાઇપિંગ સ્કીમ સરળીકરણ અને એન. એફ. એ. સરળીકરણ વચ્ચેના સંબંધને ઔપચારિક બનાવ્યો અને દર્શાવ્યું કે સબટાઇપિંગના ઔપચારિકરણ પર બીજગણિત લેવાથી એમ. એલ. જેવી ભાષા (જેને એમ. એલ. સબ કહેવાય છે) માટે કોમ્પેક્ટ મુખ્ય ટાઇપિંગ યોજનાઓ પેદા કરવાની મંજૂરી મળે છે. નોંધપાત્ર રીતે, તેમની સૂચિત ટાઇપિંગ યોજનામાં સ્પષ્ટ અવરોધોને બદલે સંઘ અને આંતરછેદના પ્રકારોના પ્રતિબંધિત સ્વરૂપનો ઉપયોગ કરવામાં આવ્યો હતો. પેરેક્સે પાછળથી દાવો કર્યો હતો કે આ બીજગણિત રચના એલ્ગોરિધમ W જેવા પ્રમાણમાં સરળ અલ્ગોરિધમની સમકક્ષ હતી, અને યુનિયન અને આંતરછેદના પ્રકારોનો ઉપયોગ આવશ્યક ન હતો. બીજી બાજુ, ઓબ્જેક્ટ-ઓરિએન્ટેડ પ્રોગ્રામિંગ ભાષાઓના સંદર્ભમાં પ્રકાર અનુમાન વધુ મુશ્કેલ સાબિત થયું છે, કારણ કે ઓબ્જેક્ટ પદ્ધતિઓને સિસ્ટમ એફની શૈલીમાં પ્રથમ-વર્ગના બહુરૂપતાની જરૂર પડે છે (જ્યાં પ્રકાર અનુમાન અનિશ્ચિત છે) અને એફ-બાઉન્ડેડ બહુરૂપતા જેવી સુવિધાઓને કારણે. પરિણામે, સબટાઇપિંગ સાથે ઓબ્જેક્ટ-ઓરિએન્ટેડ પ્રોગ્રામિંગને સક્ષમ કરતી ટાઇપ સિસ્ટમ્સ, જેમ કે કાર્ડેલીની સિસ્ટમ, એચ. એમ.-શૈલીના પ્રકાર અનુમાનને સમર્થન આપતી નથી. રો પોલીમોર્ફિઝમનો ઉપયોગ માળખાકીય રેકોર્ડ્સ જેવી સહાયક ભાષા સુવિધાઓ માટે સબટાઇપિંગના વિકલ્પ તરીકે થઈ શકે છે. જ્યારે પોલીમોર્ફિઝમની આ શૈલી કેટલીક રીતે સબટાઇપિંગ કરતાં ઓછી લવચીક છે, ખાસ કરીને પ્રકારનાં અવરોધોમાં દિશાના અભાવનો સામનો કરવા માટે સખત રીતે જરૂરી કરતાં વધુ પોલીમોર્ફિઝમની જરૂર પડે છે, તેનો ફાયદો એ છે કે તેને પ્રમાણભૂત એચ. એમ. અલ્ગોરિધમ્સ સાથે ખૂબ સરળતાથી એકીકૃત કરી શકાય છે. નોંધો સંદર્ભો બાહ્ય કડીઓ ગિટહબ પર તેના સ્રોત કોડ સાથે એલ્ગોરિધમ ડબલ્યુ નું સાક્ષર હાસ્કેલ અમલીકરણ. પાયથોનમાં હિન્દલી-મિલનર અલ્ગોરિધમનો એક સરળ અમલ. પ્રકાર પ્રણાલીઓ પ્રકાર સિદ્ધાંત પ્રકાર અનુમાન લામ્બડા કલન સૈદ્ધાંતિક કોમ્પ્યુટર વિજ્ઞાન ઔપચારિક પદ્ધતિઓ 1969 કોમ્પ્યુટિંગમાં 1978 કમ્પ્યુટિંગમાં 1985 કમ્પ્યુટિંગ અલ્ગોરિધમ્સમાં