2 पॉइंट द्वारा GN⁺ 2024-08-05 | 1 टिप्पणियां | WhatsApp पर शेयर करें
  • “Turing-complete नहीं है, इसलिए सुरक्षित है” जैसी चर्चा गणितीय अर्थ से मेल नहीं खाती; non-Turing completeness का termination, determinism और sandboxing जैसी व्यावहारिक खूबियों से ज़्यादातर अलग संबंध है
  • जिन Turing Machine computations का execution time input के लिए किसी primitive recursive function से सीमित है, उन्हें primitive recursive functions के रूप में भी फिर से लिखा जा सकता है
  • Primitive recursive functions हमेशा terminate करती हैं, लेकिन 2^(2^N) जैसी तेज़ी से बढ़ने वाली functions भी बना सकती हैं, इसलिए termination guarantee का मतलब व्यावहारिक execution time नहीं होता
  • व्यवहार में, कभी न रुकने वाले program और अरबों साल बाद खत्म होने वाले program लगभग एक जैसी समस्या पैदा करते हैं; Turing-complete languages को भी step counter से जबरन रोका जा सकता है
  • किसी configuration language की quality, उसके Turing-complete होने या न होने से ज़्यादा determinism, स्पष्ट semantics, purity, security/sandboxing, execution time control और simplicity पर निर्भर करती है

Turing-completeness चर्चा की मुख्य गलतफहमी

  • इंटरनेट पर programmers अक्सर किसी खास domain में “Turing-complete नहीं है” को advantage या requirement की तरह बताते हैं
  • लेकिन Turing completeness गणित से आया एक ठोस term है, इसलिए इसे practitioners द्वारा चाही जाने वाली कई properties के proxy के रूप में इस्तेमाल करने से अर्थ धुंधला हो जाता है
  • असल में जिन properties की ज़रूरत होती है वे termination guarantee, fast execution, deterministic behavior, sandboxing, simple configuration language जैसी चीज़ें हैं, और ये Turing completeness से ज़्यादातर orthogonal हैं
  • इस अंतर को समझने के लिए Primitive Recursive Functions (PRF) का एक सरल theoretical result ज़रूरी है

पर्याप्त तेज़ Turing Machine को PRF में बदला जा सकता है

  • Turing-complete language में लिखे program के लिए भी अगर पता हो कि उसका execution time O(2^(2^N)) से तेज़ है, तो उसी algorithm को non-Turing complete language में भी implement किया जा सकता है
  • ज़्यादातर practical problems 2^(2^N) से तेज़ खत्म होने वाले क्षेत्र में आते हैं
  • इसलिए non-Turing complete language practical computation power को meaningful तरीके से सीमित नहीं करती, और न ही computation को control करने की कोई खास क्षमता अपने-आप देती है
  • practical नज़रिए से, नीचे दिए दो programs असल में एक जैसी समस्या पैदा करते हैं
    • terminate न करने वाला program
    • ऐसा program जो 1 अरब के 1 अरब गुना जैसे steps के बाद ही terminate हो
  • Turing-complete language में भी implementation level पर steps गिनकर और एक सीमा के बाद error के साथ रोककर non-termination problem को सीधे रोका जा सकता है

FSM: हमेशा terminate करता है, लेकिन expressiveness सीमित है

  • Finite State Machine (FSM) एक recognizer है जो string को input के रूप में लेकर “yes” या “no” लौटाता है
  • FSM में finite set of states, start state, yes states का set और transition function होते हैं
  • input के हर symbol पर transition function बार-बार apply करने के बाद, final state yes state है या नहीं, इससे result तय होता है
  • FSM की expressiveness regular expression के बराबर होती है
  • FSM input length के साथ linear तरीके से चलता है और हमेशा terminate करता है, लेकिन हर string set को recognize नहीं कर सकता
    • उदाहरण के लिए 1, 010, 00100, 0001000 जैसे strings का set, जिसमें 1 के दोनों ओर बराबर संख्या में 0 होते हैं, FSM से recognize नहीं किया जा सकता
    • काफी लंबे input में states repeat होकर cycle बनता है, और उस cycle segment को duplicate करने पर FSM अब भी yes state तक पहुंचता है, लेकिन string condition टूट जाती है

Turing Machine: FSM में variable tape जोड़ने वाला model

  • Turing Machine (TM) में FSM की तरह states और transition function होते हैं, लेकिन immutable input के बजाय वह variable tape पर operate करती है
  • हर step में TM current tape symbol पढ़कर ये काम करती है
    • current symbol को नए symbol से replace करती है
    • internal state बदलती है
    • head को एक cell left या right ले जाती है
  • जब TM halt state तक पहुंचती है, तो रुक जाती है, और उस समय tape का content result होता है
  • FSM binary recognizer है, जबकि TM function compute करने वाला device है
  • TM का रुकना ज़रूरी नहीं; वह tape पर आगे-पीछे जा सकती है और state बदलती रह सकती है, फिर भी final state तक नहीं पहुंच सकती

Universal Turing Machine और computation power

  • TM का program user input के रूप में दिया गया code नहीं, बल्कि transition function खुद में hardcoded होता है
  • लेकिन किसी भी TM और input को text file के रूप में encode करके, उसे interpret करने वाली “interpreter” TM बनाई जा सकती है
  • ऐसी TM Universal Turing Machine है, जो input के रूप में दी गई दूसरी TM को simulate करती है
  • Python में TM interpreter बनाया जा सकता है, और उल्टा Python interpreter भी TM में implement किया जा सकता है, इसलिए computation power के लिहाज़ से दोनों को equivalent माना जा सकता है
  • FSM, TM से कमजोर है
    • TM, FSM को simulate कर सकती है
    • TM tape manipulation से ऐसी string को decide कर सकती है जिसमें दोनों ओर बराबर संख्या में 0 और बीच में 1 हो
    • FSM वही problem solve नहीं कर सकता

Tape को दो stacks के रूप में देखा जा सकता है

  • TM का tape एक abstraction है जिसे general programming languages में सीधे implement करना असुविधाजनक है
  • tape और head position को दो stacks से represent किया जा सकता है
    • head के left की content left stack
    • head के right की content reverse order में right stack
  • head को left या right ले जाने की operation एक stack से pop करके दूसरे stack में push करने में बदल जाती है
  • इसलिए TM की computation power “दो stacks वाले FSM” के बराबर होती है
  • अगर stack symbols केवल 0 और 1 हों, तो stack को एक natural number से भी represent किया जा सकता है
    • top check: stack % 2
    • pop: stack / 2
    • push x: stack * 2 + x

Turing Machine की सीमा: Halting Problem और Rice-type results

  • हर TM को text के रूप में encode किया जा सकता है, इसलिए संभावित TMs को infinite list में enumerate किया जा सकता है
  • diagonalization argument का इस्तेमाल करके दिखाया जा सकता है कि कुछ functions TM से compute नहीं की जा सकतीं
  • इसका अधिक concrete उदाहरण Halting Problem है
    • TM का source code और input दिए जाने पर, यह decide करने की problem कि वह TM कभी रुकेगी या नहीं
  • अगर मान लें कि halts(program, input) हमेशा सही तरह से terminate करता है, तो weird program में contradiction पैदा होता है, जो input के रूप में अपना ही source code लेता है
    • अगर वह रुकने का फैसला करता है, तो infinite loop में चला जाता है और नहीं रुकता
    • अगर वह न रुकने का फैसला करता है, तो तुरंत terminate करता है
  • इसलिए halts को कुछ cases में गलत होना पड़ेगा, या कुछ cases में terminate नहीं करना पड़ेगा
  • अधिक general रूप में, किसी भी TM के लिए behavior-preserving non-trivial property को algorithmically decide नहीं किया जा सकता
    • syntactic properties check की जा सकती हैं, लेकिन refactoring के बाद भी बनी रहने वाली behavioral properties आम तौर पर decidable नहीं होतीं

Primitive recursive functions: हमेशा terminate करने वाला computational device

  • Primitive Recursive Function (PRF) को ऐसी function के रूप में define किया जाता है जो natural numbers के tuple को लेकर एक natural number लौटाती है
  • basic functions zero और succ हैं
    • zero = 0
    • succ(x) = x + 1
  • function composition से constants बनाए जा सकते हैं
    • succ(zero) = 1
    • succ(succ(zero)) = 2
  • general recursion allowed नहीं है, लेकिन fixed iteration count वाला limited loop LOOP(init, f, n) allowed है
    • LOOP(init, f, 0) = init
    • LOOP(init, f, 1) = f(init)
    • LOOP(init, f, 2) = f(f(init))
  • मुख्य constraint यह है कि iteration count n loop start होने से पहले fixed होता है, और loop body में loop counter बदला नहीं जा सकता

PRF से basic programming constructs बनाना

  • addition को add(x, y) = LOOP(x, succ, y) के रूप में define किया जा सकता है
  • multiplication को mul(x, y) = LOOP(0, add x, y) के रूप में define किया जा सकता है
  • exponentiation को pow(x, y) = LOOP(1, mul x, y) के रूप में define किया जा सकता है
  • इससे तेज़ी से बढ़ने वाली functions भी बनाई जा सकती हैं
    • pow_2(n) = pow(2, n)
    • pow_2_2(n) = pow_2(pow_2(n))
  • basic functions में pred जोड़ने पर saturated subtraction और boolean operations बनाए जा सकते हैं
    • sub(x, y) = LOOP(x, pred, y)
    • and(x, y) = mul(x, y)
    • not(x) = sub(1, x)
    • if(cond, a, b) को भी arithmetic expression से represent किया जा सकता है
  • comparison operations, remainder और division को भी bounded iteration और conditionals के जरिए implement किया जा सकता है

PRF की data structures और TM simulation

  • PRF कई arguments ले सकती है, लेकिन result एक natural number होता है, इसलिए data structures को natural number में encode करना पड़ता है
  • pair (a, b) को 2^a * 3^b से represent किया जा सकता है
  • components निकालने के लिए किसी खास prime का maximum exponent ढूंढना होता है
    • fst(p) वह maximum power exponent है जिससे 2 p को divide करता है
    • snd(p) वह maximum power exponent है जिससे 3 p को divide करता है
  • इसी तरह तीन values (S, stack1, stack2) को भी एक natural number में pack किया जा सकता है
  • TM configuration को नीचे दिए तीन elements से represent किया जा सकता है
    • current state S
    • tape का left stack
    • tape का right stack
  • stack manipulation remainder, multiplication और division से implement किया जा सकता है, इसलिए TM का single step PRF में encode किया जा सकता है
  • LOOP(initial_config, single_step, n) का इस्तेमाल करके TM को ठीक n steps तक simulate किया जा सकता है
  • समस्या यह है कि पर्याप्त n पता नहीं होता, लेकिन अगर execution time किसी PRF से bounded है, तो उतनी बार iterate करने के लिए बनाया जा सकता है
  • आखिरकार, जिस TM computation का execution time primitive recursive function से bounded है, उसे PRF से replace किया जा सकता है

PRF की सीमा: हमेशा terminate करने पर भी TM जितनी powerful नहीं

  • PRF हमेशा terminate करती है, लेकिन सभी terminating functions को express नहीं करती
  • ऐसी functions मौजूद हैं जिन्हें TM compute कर सकती है, लेकिन PRF compute नहीं कर सकती
  • इसे दिखाने के लिए PRF syntax tree की depth के आधार पर growth-rate upper bound तय किया जाता है
  • depth d या उससे कम वाली PRF को एक खास unary function A_d से तेज़ी से न बढ़ने के लिए bound किया जा सकता है
  • A(d, x) इस तरह define होता है
    • A(1, x) = x + 1
    • A(d + 1, 0) = A(d, A(d, 0))
    • A(d + 1, x) = A(d, A(d + 1, x - 1))
  • इस definition में हर recursive call में (d, x) lexicographic रूप से छोटा होता है, इसलिए TM पर compute करने पर terminate करता है
  • a(x) = A(x, x) किसी भी PRF से तेज़ी से बढ़ता है, और TM से compute किया जा सकता है लेकिन PRF से नहीं

व्यवहार में लौटें: सिर्फ non-Turing completeness काफी नहीं

  • Turing Machine रुकने में fail हो सकती है
  • FSM और PRF जैसे हमेशा terminate करने वाले devices भी fast खत्म होने की guarantee नहीं देते
  • PRF 2^(2^N) जैसी बड़ी functions compute कर सकती है, इसलिए सिर्फ termination guarantee practical execution time की guarantee नहीं देती
  • वास्तविक दुनिया के कई algorithms का execution time PRF से bounded होता है, इसलिए उन्हें non-Turing complete device से भी express किया जा सकता है
  • Turing-complete computation को PRF जैसा बनाने का सामान्य तरीका iteration counter जोड़ना है, और counter बहुत बड़ा होने पर जबरन रोक देना है

Configuration language में सच में ज़रूरी properties

  • Configuration language अक्सर “non-Turing complete” को design goal के रूप में पेश करती है, लेकिन असल में इससे stronger कई properties चाहिए होती हैं
  • Determinism

    • Configuration language deterministic होनी चाहिए
    • Python के id([]) की तरह हर run में अलग value देने वाला behavior general programming में acceptable हो सकता है, लेकिन configuration के लिए inappropriate है
    • Configuration अक्सर incremental builds या caching systems की key के रूप में इस्तेमाल होती है, इसलिए nondeterminism आने पर cache behavior अस्थिर हो जाता है
  • स्पष्ट semantics

    • language behavior को referenceable standard के रूप में स्पष्ट रूप से fixed होना चाहिए
    • ASLR बंद करके और खास allocator इस्तेमाल करके Python के id([]) को deterministic बनाया जा सकता है, लेकिन यह guarantee नहीं होती कि result predictable होगा या implementations के बीच same होगा
    • अलग implementation या Python version changes में भी same behavior guarantee करने के लिए semantics स्पष्ट होना चाहिए
  • Purity

    • अगर configuration environment variables या disk files पढ़ सकती है, तो configuration का meaning evaluation environment पर depend करता है
    • caching सही तरह काम करे, इसके लिए configuration language में purity होनी चाहिए
  • Security और sandboxing

    • purity और security दोनों general IO expose न करने के तरीके से हासिल किए जा सकते हैं
    • दोनों properties का purpose अलग है
    • purity result को nondeterministic होने से रोकने के लिए है
    • security attacker को access tokens जैसे resources expose न करने के लिए है
  • Execution time control

    • IO control करने पर भी malicious configuration CPU जलाने वाला denial of service attack कर सकती है
    • execution time guarantee के लिए दो approaches इस्तेमाल की जा सकती हैं
    • processing को input size के सीधे proportional स्पष्ट linear structure तक सीमित करना
    • metered execution इस्तेमाल करना, जिसमें हर atomic step पर counter घटता है और counter 0 होने पर execution रुक जाता है
  • Simplicity

    • Configuration language को users को simple programs लिखने के लिए encourage करना चाहिए
    • recursion और infinite loops को ban करना simplicity की तरफ speed bump बन सकता है
    • हालांकि PRF example की तरह, ऐसे bans मनमाने recursive programs लिखने को पूरी तरह नहीं रोकते; बस indirect code की ज़रूरत पड़ती है
    • संबंधित उदाहरण के रूप में some roundabout code देखा जा सकता है

अंतिम सार

  • जिस Turing Machine algorithm का input के लिए execution time किसी primitive recursive function से bounded है, उसे primitive recursive function से भी implement किया जा सकता है
  • non-Turing completeness termination guarantee जैसी एक property दे सकती है, लेकिन practical execution time upper bound या configuration language quality की guarantee अपने-आप नहीं देती
  • Configuration language design में अहम मुद्दे Turing completeness खुद नहीं, बल्कि determinism, स्पष्ट semantics, purity, sandboxing, execution time metering और simplicity हैं

1 टिप्पणियां

 
GN⁺ 2024-08-05
Hacker News की राय
  • अपना प्रमोशन: https://www.nayuki.io/page/primitive-recursive-functions

    • मूल लेख से काफी बेहतर है, लेकिन लगता है आजकल सभी ELI5-स्टाइल आसान व्याख्या को ज्यादा पसंद करते हैं
  • लेख के निष्कर्ष वाले हिस्से में configuration language से जुड़े कुछ काफी अच्छे मानदंड हैं, और मैं सोच रहा हूं कि मौजूदा भाषाओं में कोई ऐसी है जो इन सब या ज्यादातर मानदंडों को पूरा करती हो

    • इन मानदंडों को पूरा करने वाले उदाहरणों में Dhall [1] और Cue [2] हैं, लेकिन एक मायने में ये बहुत रोचक उदाहरण नहीं हैं
      Dhall जानबूझकर एक total functional language है, इसलिए वह “Turing-complete न होने” की दिशा में जाती है, और Cue में functions नहीं हैं, इसलिए recursion करने के लिए भी कुछ नहीं है
      मुझे लगता है RCL [3] मानदंडों को पूरा करती है। यह deterministic और pure है, metered execution देती है, और filesystem access को sandbox करती है। अगर sandbox policy अनुमति दे तो files पढ़ी जा सकती हैं, लेकिन ऐसी files को source code का हिस्सा माना जाता है और वे import की तरह ही काम करती हैं
      RCL में लेखक द्वारा बताए गए कारणों से मैं “Turing-complete न होने” की दिशा में नहीं जाना चाहता था। यह तथ्य कि program आखिरकार terminate होगा, practical काम में बहुत उपयोगी property नहीं है; उल्टा, Agda जैसी total functional languages में भी बहुत complex programs लिखे जा सकते हैं, इसलिए non-Turing-completeness सरल programs/configuration की गारंटी नहीं देती
      RCL के सभी loops bounded हैं, लेकिन functions होने की वजह से recursion भी संभव है। Tail calls नहीं हैं, इसलिए शुरुआत में native stack overflow रोकने के लिए recursion depth limit लगाई थी, लेकिन fuzzer ने ऐसा function ढूंढ निकाला जो constant stack space में चलते हुए भी रुक जाता था, और मैं अभी तक उसे पूरी तरह नहीं समझ पाया हूं: let f = g => g(g(h => k => g(g(h)))); f(f)
      आखिरकार, ऐसे pathological functions को express कर पाना practical तौर पर समस्या नहीं है। Execution steps की limit, यानी “gas limit” या लेखक की कही “metered execution”, रखी जा सकती है। Code को simple बनाए रखने में built-in iteration structures का bounded होना और recursion का असुविधाजनक होना एक अच्छा nudging mechanism है, लेकिन अंततः सबसे मूल्यवान tools code review और अच्छा judgment ही हैं
      [1]: https://dhall-lang.org/
      [2]: https://cuelang.org/
      [3]: https://rcl-lang.org/
    • यह imperative है और “pure” भी नहीं, लेकिन C तक को इस दिशा में बनाया गया था कि किसी भी loop में जाने से पहले iterations की upper bound पता चल सके, और इसी वजह से वह primitive recursive है
      Dennis Ritchie का MIT research उस विषय पर केंद्रित था जिसे वे loop programming कहते थे
      The complexity of loop programs - ALBERT R. MEYER and DENNIS M. RITCHIE
      https://people.csail.mit.edu/meyer/meyer-ritchie.pdf
      लगभग हर आधुनिक programmer जिस structured programming को default रूप से अपनाता है, वह असल में primitive recursive functions की तरफ धकेलने वाला paradigm है। शायद इसलिए Dijkstra के “goto considered harmful” paper को लेकर भ्रम होता है, क्योंकि structured programming pop, functional जैसे अन्य दो प्रकारों की तुलना में लगभग universal रूप से स्वीकार कर ली गई है
      Primitive recursive functions सभी computable functions को include नहीं करते, लेकिन termination-guaranteed intuitive functions में से लगभग सभी को include करते हैं। बेशक, ऐसे loops की वास्तव में जरूरत पड़ सकती है जिनमें loop में enter करते समय iteration count पता न हो, लेकिन यह ऐसी footgun है जिसे केवल सच में जरूरत पड़ने पर इस्तेमाल किया जाए तो टाला जा सकता है
      COBOL तक ने unlimited goto को ALTER command में shift करके modernize किया था। कोई आधुनिक और उपयोगी language याद नहीं आती जो PR functions की अनुमति न देती हो
      C में भी अगर while से बचते हुए और fall through को स्पष्ट रूप से avoid करते हुए लिखा जाए, तो लगभग हमेशा ऐसा total-function code बनाया जा सकता है जो निश्चित रूप से terminate हो
      ML की type inference जैसे pathological cases भी हैं। Complexity class की तुलना में वास्तविक cost काफी सस्ती होती है, इसलिए भले ही language total function न हो और ऐसे उपयोग को restrict करना कठिन हो, फिर भी इसे स्वीकार करना worth it है
      Practical तौर पर देखें तो सभी languages आम तौर पर ऐसे ज्यादातर मानदंडों को support करने वाले defaults देती हैं, लेकिन इन्हें enforce करने वाली constraints language की उपयोगिता को गंभीर रूप से सीमित कर देंगी। यहां तक कि आलोचना झेलने वाले SOLID और Clean frameworks भी मुझे इसी model की तरफ धकेलते दिखते हैं
      Structured programming इतनी universal हो चुकी है कि यह बात भूलना आसान है, और कभी-कभी इसे सिखाया भी नहीं जाता। एक बूढ़े दाढ़ीवाले के तौर पर मुझे याद है कि WHILE आदि के खतरों के बारे में सीखा था
    • Dhall को चुनकर देख सकते हैं कि वह किन मानदंडों पर fail होती है। सबसे करीब लगती है
  • O(2^(2^N)) से तेज चलता है कहना शायद simplification की कोशिश रही होगी, लेकिन “बहुत बड़ी संख्या” वाला हिस्सा भरोसा थोड़ा कम करता है
    सही तौर पर शायद “बहुत तेजी से बढ़ने वाला function” कहना चाहिए। या फिर मतलब यह लगता है कि program O(2^(2^N)) steps से कम में खत्म होता है

  • अगर सिर्फ़ पहले हिस्से को देखें, जहाँ कहा गया है कि सीमित language कुछ applications के लिए बेहतर है, तो मुझे लगता है कि इसका फ़ायदा यह है कि ज़रूरी steps की संख्या का upper bound statically calculate किया जा सकता है
    तब किसी भी input के लिए limit का उल्लंघन करने वाली computation को reject करके meaningful error लौटाया जा सकता है
    इसके उलट, Turing-complete language पर runtime limit लगाने का तरीका कुछ ऐसे inputs के लिए limit बहुत कम रख सकता है जिनमें हमारी दिलचस्पी है। इसे run करके limit hit होने तक पता नहीं चलता। C++ template recursion में ऐसा कभी-कभी दिखता है
    हो सकता है मैं पूरी तरह confuse होऊँ, इसलिए कोई ज़्यादा जानकार समझा दे तो अच्छा होगा

    • मेरे एक पुराने colleague ने limit को लगभग 3x रखा था, और कुछ साल बाद real workload उस limit से टकराने के बाद से मैं reasonable computation amount की 10x limit इस्तेमाल करता हूँ
      खराब workflow को fail होने में कुछ गुना ज़्यादा समय लगे, तब भी वह millisecond range में ही रहता है, इसलिए मुझे नहीं लगता कि बड़ा नुकसान है
      आम तौर पर यह समस्या तब आती है जब कोई problem domain को directed acyclic graph की तरह treat करता है, लेकिन “acyclic” enforce नहीं कर पाता। Problem को directed acyclic graph के रूप में model करना ऐसा है जैसे Dark Galadriel Frodo से ring लेने पर विचार कर रही हो। “सब मुझे प्रेम करेंगे और निराश होंगे।” ऐसी चीज़ें बनाने वाले लोग हमेशा उन चीज़ों पर उससे कहीं ज़्यादा गर्व करते हैं जितना उन्हें करना चाहिए
      आखिर में महंगे और जटिल solution में खिंचकर आए customers का पैसा खत्म हो जाता है, और उनकी अपनी समस्या भी बहुत छोटी दिखने लगती है। तब सचमुच सिर्फ़ वही app बचती है जो per-task cost को इतना कम नहीं रख सकती कि customer का business चल सके
    • blockchain computation के fuel usage का सटीक अनुमान लगाना दूसरों के लिए दिलचस्प हो सकता है, मेरे लिए नहीं
      मुझे तो यह static type checking, null न होना, mutation न होना जैसे पहले वाले हथौड़ों से बच निकले bugs पकड़ने के लिए toolbox का एक और हथौड़ा बनाने में ज़्यादा दिलचस्पी है
      finite time में terminate होना correctness prove नहीं करता, लेकिन अगर मैं declare करूँ कि code finite time में terminate होता है और compiler सहमत न हो, तो मैं मानूँगा कि वह code गलत है
    • Statically determined upper bound common case के actual runtime complexity को बहुत ज़्यादा overestimate कर सकता है। क्योंकि recursion में early exit कराने वाली conditionals कैसे evaluate होंगी, इसे आम तौर पर predict नहीं किया जा सकता
      early exit का runtime पर असर होना है तो lazy evaluation या short-circuit conditionals मानने होंगे, लेकिन practical language में आम तौर पर ये होते ही हैं
    • अगर वह bound बेहद ढीला हो तो क्या करेंगे? उदाहरण के लिए deterministic quick sort आम तौर पर n log n होता है, लेकिन input size के लिहाज़ से इसका quadratic upper bound होता है
      तो क्या quick sort computation reject करेंगे? और ज़्यादा extreme रूप में, Hindley–Milner algorithm का exponential time upper bound है, लेकिन व्यवहार में अक्सर linear time में चलता है
    • मुझे नहीं पता कि यह “statically calculate” होता है या नहीं, लेकिन language capability को बहुत सीमित करने का एकमात्र फ़ायदा मुझे यही लगता है कि data पर निर्भर न करने वाली computation limit लगाई जा सकती है
      हालांकि ऐसी कोई स्थिति याद करना मुश्किल है जहाँ यह वाकई strong requirement हो। कितने systems ऐसे हैं जो “query बहुत देर तक चली” error नहीं दे सकते?
  • मैं terminate न करना / bounded होना principle पर आधारित backend web programming language आज़माना चाहता था
    कल्पना यह है कि compiler हर function के लिए prove करे कि दिए गए state और arguments पर execution bounds के भीतर है, और X lower bound है व Y upper bound, यह दिखाया जा सके। यह जानकारी entry point तक propagate होती है
    लेखक की इस बात से सहमत हूँ कि ज़्यादा strong semantics चाहिए, और इसी वजह से मैंने इस language के बारे में सोचा था। Program execution time की guarantees अक्सर चाहिए होती हैं
    मूल आधार primitive recursive functions होगा, लेकिन व्यवहार में यह Turing-complete हो सकती है। जैसे Rust गलत borrow को reject करता है लेकिन raw pointers के लिए unsafe देता है, वैसे ही यह language भी simple iteration primitives के आधार पर upper bound calculate करेगी, या unsafe operator इस्तेमाल करके bounds के लिए alternative formula देने देगी

  • लेख की छोटी-सी शिकायत/प्रेरणा वाला हिस्सा ठीक से समझ नहीं आया
    मेरा मतलब इस हिस्से से है: “आम तौर पर कुछ domains में Turing-complete न होना benefit या requirement के रूप में सराहा जाता है। मुझे लगता है ऐसी ज़्यादातर चर्चाएँ गलत समझ पर आधारित हैं — Turing-complete न होना वह अर्थ नहीं रखता जो लोग उम्मीद करते हैं”
    ऐसी चर्चाएँ गलत क्यों हैं? ज़्यादातर formal analysis tools, जैसे Coq, Isabelle, Agda, आम तौर पर proof मांगते हैं कि function terminate करता है। यह साबित करने जैसा ही है कि वह function total function है, और इसलिए क्या इसका मतलब यह नहीं कि वह primitive recursive है?

    • मैंने अंत तक नहीं पढ़ा, लेकिन लगता है यह लेख कुछ configuration languages द्वारा “Turing-complete नहीं” को feature बताने से निकला है। असल में जिस feature का प्रचार करना चाहिए वह शायद reasonably bounded execution time है
      हाल की CEL-related discussion में भी यह आया था:
      https://news.ycombinator.com/item?id=40954652
    • अगर बात formal proofs की है, तो modern programming में इस्तेमाल होने वाले scientific counterexamples की नहीं, बल्कि general case में यह prove करना कि function total है, एक NP-complete search problem है
      अगर याद सही है तो यह co-NP oracle वाला NP है, या polynomial hierarchy के दूसरे level के equivalent है। छोटे problems में संभव हो तो भी महंगा है
      ये tools सबसे अच्छा तब काम करते हैं जब program को total function बनने के लिए structure किया जाए। उनमें structural programming में सिर्फ़ FOR इस्तेमाल करना, या bounded iteration count वाला WHILE/recursion इस्तेमाल करना सबसे आम तरीका है
      हालांकि इसका संबंध सिर्फ़ SAT से है, Schaefer’s dichotomy theorem में आने वाले tractable forms मुझे सबसे accessible lens लगते हैं
    • जैसा लेख दिखाता है, terminate करने वाले लेकिन primitive recursive न होने वाले functions मौजूद हैं, इसलिए total function proof का मतलब primitive recursive होना नहीं है
      Agda और शायद दूसरे tools भी कुछ terminating non-primitive recursive functions के लिए termination prove कर सकते हैं। बेशक सभी के लिए यह संभव नहीं है
      लेख जिस गलतफहमी की शिकायत करता है, वह मोटे तौर पर ऐसी लगती है: “Turing-completeness का मतलब computation कर पाना है, और non-Turing-completeness का मतलब computation न कर पाना और अच्छी configuration language properties होना है।”
      लेख का point यह है कि non-Turing-complete होने पर भी बहुत costly या tricky काम किए जा सकते हैं, और configuration language के लिए सिर्फ़ non-Turing-complete होने से कहीं ज़्यादा strict limits चाहिए
    • non-Turing-complete होने के तरीके सिर्फ़ साफ़-सुथरे ढंग से terminate करने वाले total functions बनने तक सीमित नहीं हैं। उदाहरण के लिए infinite loop universal computation भी नहीं कर सकता और terminate भी नहीं करता
  • मैं CUE डेवलपर हूँ। CUE primitive recursive है, और एक “अच्छी” configuration language से अपेक्षित मानकों को भी पूरा करता है