4.6. حل‌وفصل Derivation

به ضمیمه این فصل درباره دستور زبان و قراردادهای فرامتغیر (metavariable) مراجعه کنید.

تفکیک (resolve) یک derivation عبارت است از جایگزین کردن ورودی‌های آن با ساده‌ترین ورودی‌ها — یعنی مسیرهای انبار ساده — که به همان اشیاء انبار اشاره دارند.

derivationهایی که فقط مسیرهای انبار را به عنوان ورودی دارند نیز به همین ترتیب derivationهای تفکیک‌شده نامیده می‌شوند. (آن‌ها به این دلیل چنین نامیده می‌شوند که چه در واقع خروجی تفکیک derivation باشند و چه از ابتدا بدون ورودی‌های غیرمسیر انبار به این شکل درآمده باشند.)

هم‌ارزی محتوای ورودی derivationها

مسیرهای مشتق‌شونده عمداً این امکان را فراهم می‌کنند که به یک شیء انبار به روش‌های مختلفی اشاره شود. این پیامد آدرس‌دهی مبتنی بر محتوا است، از آنجا که derivationهای مختلف می‌توانند خروجی‌های یکسانی تولید کنند، و داده‌های یکسان را نیز می‌توان به صورت دستی به انبار اضافه کرد. این همچنین حتی پیآمد آدرس‌دهی مبتنی بر ورودی است، زیرا می‌توان به یک خروجی با نام derivation و خروجی، یا مستقیماً توسط مسیر انبار محاسبه‌شده‌اش ارجاع داد. از آنجا که ارجاع‌زدایی (dereferencing) مسیرهای مشتق‌شونده بدین ترتیب تزریقی (injective) نیست، یک رابطه هم‌ارزی را روی مسیرهای مشتق‌شونده القا می‌کند.

بیایید این رابطه هم‌ارزی را \(\sim\) بنماییم، که در آن \(p_1 \sim p_2\) به این معناست که مسیرهای مشتق‌شونده‌ی \(p_1\) و \(p_2\) به یک شیء انبار یکسان اشاره دارند.

هم‌ارزی محتوا: دو مسیر مشتق‌شونده در صورتی هم‌ارز هستند که به یک شیء انبار اشاره کنند:

\[ \begin{prooftree} \AxiomC{${}^p_1 = {}^p2$} \UnaryInfC{$p_1 \,\sim\mathrm{DP}\, p_2$} \end{prooftree} \]

که در آن \({}^*p\) نشان‌دهنده‌ی شیء انباری است که مسیر مشتق‌شونده‌ی \(p\) به آن اشاره دارد.

این امر همچنین یک رابطه هم‌ارزی را بر روی مجموعه‌هایی از مسیرهای مشتق‌شونده القا می‌کند:

\[ \begin{prooftree} \AxiomC{$\{ {}^p | p \in P_1 \} = \{ {}^p | p \in P2 \}$} \UnaryInfC{$P_1 \,\sim{\mathcal{P}(\mathrm{DP})}\, P_2$} \end{prooftree} \]

هم‌ارزی محتوای ورودی: این امر به نوبه خود، یک رابطه هم‌ارزی را روی derivationها القا می‌کند: دو derivation در صورتی هم‌ارز هستند که ورودی‌های آن‌ها هم‌ارز باشد و در غیر این صورت با هم برابر باشند:

\[ \begin{prooftree} \AxiomC{$\mathrm{inputs}(d1) \,\sim{\mathcal{P}(\mathrm{DP})}\, \mathrm{inputs}(d2)$} \AxiomC{$ d_1\left[\mathrm{inputs} := \{\}\right] \= d_2\left[\mathrm{inputs} := \{\}\right] $} \BinaryInfC{$d_1 \,\sim\mathrm{Drv}\, d_2$} \end{prooftree} \]

تفکیک derivation همیشه derivationها را به derivationهای هم‌ارز با محتوای ورودی نگاشت می‌کند.

رابطه تفکیک

ارجاع‌زدایی از یک مسیر مشتق‌شده — یعنی همان \({}^*p\) در بالا — صرفاً به عنوان یک جعبه سیاه معرفی شد. اما در واقع این یک فرآیند چندمرحله‌ای برای جستجوی نتایج ساخت در ردپای ساخت است که خود به تفکیک کلیدهای جستجو بستگی دارد. بنابراین، تفکیک یک فرآیند بازگشتی چندمرحله‌ای است که رسم نمودار رسمی برای آن ارزشمند است.

ما می‌توانیم این کار را با یک رابطه انتقال دوتایی گام‌کوچک انجام دهیم؛ بیایید آن را \(\rightsquigarrow\) بنماییم. سپس می‌توانیم برابری ارجاع‌زدایی‌شده را به این صورت نتیجه‌گیری کنیم:

\[ \begin{prooftree} \AxiomC{$p_1 \rightsquigarrow^p$} \AxiomC{$p_2 \rightsquigarrow^ p$} \BinaryInfC{${}^p_1 = {}^p_2$} \end{prooftree} \]

즉 یعنی با نشان دادن اینکه هر دو مورد اصلی (طی صفر یا چند گام کوچک، از این رو علامت \({}^*\)) به دقیقاً همان مورد یکسان تفکیک می‌شوند.

با این انگیزه، اکنون بیایید یک سیستم گام‌کوچک از قوانین کاهشی را برای تفکیک، به شکل رسمی درآوریم.

قوانین رسمی

رابطه تک‌عملوندی (unary) \(\text{resolved}\)

\[ \begin{prooftree} \AxiomC{$s \in \text{store-path}$} \UnaryInfC{$s$ resolved} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$\forall i \in \mathrm{inputs}(d). i \text{ resolved}$} \UnaryInfC{$d$ resolved} \end{prooftree} \]

\(\rightsquigarrow\) رابطه دودویی

نکته

در واقع، برای کاملاً صوری بودن، لازم است ردپای ساخت (build trace) را که می‌خواهیم حل (resolve) را بر اساس آن انجام دهیم، پیگیری کنیم.

می‌توانیم این کار را با تبدیل \(\rightsquigarrow\) به یک رابطه سه‌دویی (ternary) انجام دهیم؛ به طوری که ردپای ساخت را به خودش منتقل کند تا در نهایت در آن قانون خاص از آن استفاده کند. این کار بیشتر باعث شلوغی می‌شود تا افزایش بینش، به همین دلیل زحمت نوشتن آن را به خود ندادیم.

گزینه‌های دیگری نیز وجود دارد؛ مانند این که بگوییم کل سیستم قانون کاهشی (reduction rule system) نسبت به ردپای ساخت پارامتری شده است، که اساساً کاریینگ رابطه سه‌دویی \(\rightsquigarrow\) به تابعی از ردپای‌های ساخت به رابطه دودویی نوشته‌شده در بالا است.

قانون اصلی جستجوی ردپای ساخت

\[ \begin{prooftree} \AxiomC{$s \in \text{store-path}$} \AxiomC{${}^s \in \text{derivation}$} \AxiomC{${}^s$ resolved} \AxiomC{$\mathrm{build\text{-}trace}[s][o] = t$} \QuaternaryInfC{$(s, o) \rightsquigarrow t$} \RightLabel{\scriptsize output path resolution} \end{prooftree} \]

قوانین استقرایی

\[ \begin{prooftree} \AxiomC{$i \rightsquigarrow i'$} \AxiomC{$i \in \mathrm{inputs}(d)$} \BinaryInfC{$d \rightsquigarrow d[i \mapsto i']$} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$d \rightsquigarrow d'$} \UnaryInfC{$(\mathrm{path}(d), o) \rightsquigarrow (\mathrm{path}(d'), o)$} \end{prooftree} \]

\[ \begin{prooftree} \AxiomC{$p \rightsquigarrow p'$} \UnaryInfC{$(p, o) \rightsquigarrow (p', o)$} \end{prooftree} \]

ویژگی‌ها

مانند تمام روابط ارزیابی خوش‌رفتار، حل جزئی همگرا (confluent) است. همچنین، اگر بستار تقارنی \(\rightsquigarrow^*\) را در نظر بگیریم، به روابط هم‌ارزی بخش قبلی می‌رسیم. حل (resolution)، هم‌ارزی محتوا را برای مسیرهای مشتق‌شونده و هم‌ارزی محتوای ورودی را برای derivationها رعایت می‌کند.

نکته

ما تصمیم گرفتیم که یک رابطه تک‌دویی (unary) «resolved» را از ابتدا و به طور صریح در بالا تعریف کنیم. اما می‌توان آن را به عنوان فرم‌های نرمال رابطه \(\(\rightsquigarrow^*\)\) نیز تعریف کرد:

\[ a \text{ resolved} \Leftrightarrow \forall b. b \rightsquigarrow^* a \Rightarrow b = a\]

به زبان ساده، عبارت‌های حل‌شده (resolved) عبارت‌هایی هستند که \(\rightsquigarrow^*\) آن‌ها را در سمت چپ تنها به همان عبارت در سمت راست مرتبط می‌کند؛ آن‌ها عبارت‌هایی هستند که دیگر نمی‌توانند بیشتر از این حل شوند.

حل جزئی در برابر حل کامل

مشابه ارزیابی، می‌توانیم درباره حل جزئی در برابر کامل derivation صحبت کنیم. حل جزئی derivation همان چیزی است که در بالا با \(\rightsquigarrow^*\) به شکل صوری درآورده‌ایم. حل کامل، حل‌شدنی است که به یک عبارت حل‌شده (مسیر مشتق‌شونده یا derivation) ختم می‌شود. (که بر اساس نکته بالا، یک فرم نرمال از رابطه است.)

با تفکیک نسبی (partial resolution)، یک derivation به derivationهای معادل با ورودی‌های یکسان یا ساده‌تر مرتبط می‌شود، اما همهٔ آن ورودی‌ها مسیرهای انبار ساده نخواهند بود. این امر زمانی مفید است که ورودی به یک خروجی آدرس‌دهی‌شده بر اساس محتوای شناور اشاره دارد که هنوز آن را نساخته‌ایم — ما نمی‌دانیم چه مسیر انباری (بر اساس آدرس محتوا) برای آن derivation استفاده خواهد شد، بنابراین در تلاش برای تفکیک مسیر در حال ساختِ مورد نظر، «متوقف» می‌مانیم. (در فرمالیسم بالا، این اتفاق زمانی رخ می‌دهد که ردپای ساخت کلیدهایی را که می‌خواهیم در آن جستجو کنیم، نداشته باشد.)

تفکیک کامل (complete resolution) یک رابطهٔ تابعی است، یعنی مقادیر سمت چپ به‌طور منحصربه‌فردی با مقادیر سمت راست مرتبط هستند. با این حال، این یک رابطهٔ کامل نیست (به‌طور کلی، با فرض وجود ردپاهای ساخت دلخواه). این موضوع در بخش بعدی مورد بحث قرار می‌گیرد.

خاتمه (Termination)

برای گراف‌های derivation ایستا، تفکیک کامل در واقع کامل است، زیرا همیشه برای تمام ورودی‌ها خاتمه می‌یابد. (رابطه‌ای که هم کامل و هم تابعی باشد، یک تابع است.)

با این حال، برای گراف‌های derivation پویا، این‌گونه نیست — تضمینی وجود ندارد که تفکیک خاتمه یابد. مسئله، بازنویسی خود مسیرهای در حال ساخت نیست: یک بازنویسی منفرد برای عادی‌سازی یک مسیر derivation خروجی به یک مسیر ثابت همیشه وجود دارد و همیشه در یک مرحله انجام می‌شود. مسئله این است که derivationهای پویا (یعنی آنهایی که توسط یک تفکیک قبلی در گراف پر می‌شوند) ممکن است وابستگی‌های گذای (transitive) بیشتری نسبت به derivation اصلی داشته باشند.

مثال

فرض کنید این مسیر در حال ساخت را داریم

{
  "drvPath": {
    "drvPath": "...-foo.drv",
    "output": "bar.drv"
  },
  "output": "baz"
}

و درایویشن foo از قبل حل شده است. وقتی مسیر deriving را حل می‌کنیم، در نهایت به چیزی شبیه به این خواهیم رسید.

{
  "drvPath": "...-foo-bar.drv",
  "output": "baz"
}

تا اینجا این کار صرفاً یک بازنویسی اتمی منفرد است، بدون هیچ‌گونه مشکل خاتمه‌نیافتگی. اما derivation به نام foo-bar ممکن است ورودی‌های derivation پویای مستقل خودش را داشته باشد. فرآیند تفکیک (Resolution) باید ابتدا آن derivation را حل‌وفصل کند تا در نهایت مسیر deriving ذکرشده در بالا بتواند به یک مسیر انبار ساده‌ی ...-foo-bar-baz نرمال‌سازی شود.

نکته‌ی مهمی که باید به آن توجه کرد این است که در حالی که کلیدهای «ردیابی ساخت» (build trace) باید حل‌وفصل شوند، مقداری که این کلیدها به آن نگاشت می‌شوند چنین محدودیت‌هایی ندارد. یک شیء انبار دلخواه هیچ مفهومی تحت عنوان حل‌وفصل‌شده بودن یا نبودن ندارد. اما، یک شیء انبار دلخواه را می‌توان به عنوان یک derivation دوباره خواند (همان‌طور که در واقع برای derivationهای پویا / مسیرهای deriving خروجی تو در تو انجام خواهد شد). و نیازی نیست که آن derivationها حل‌وفصل شوند.

این derivationهای پویای حل‌وفصل‌نشده هستند که منبع عدم خاتمه (non-termination) به شمار می‌روند. به همین ترتیب، آن‌ها دلیل اصلی قدرت بیان بالاتر derivationهای پویا نیز هستند.

nix.dev/manual/nix/stable/store/resolution.html