نظریه مک‌ناتون

در نظریه اتوماتا (به انگلیسی: Automata theory) نظریه مک‌ناتون (به انگلیسی: McNaughton's theorem) اشاره دارد به قضیه‌ای که بیان می‌دارد مجموعه‌ای از زبان‌های ω-منظم برابر خواهد بود با مجموعه‌ای که توسط ماشین مولر (به انگلیسی: Muller Automata) قطعی تشخیص داده شود. برای اثبات این قضیه الگوریتمی ارائه می‌شود که در آن برای هر زبان ω-منظم یک ماشین مولر قطعی ساخته می‌شود و بالعکس. این قضیه نتایج مهم و متعددی دارد. از آنجایی که ماشین بوچی (به انگلیسی: Büchi automaton) و زبان‌های ω-منظم هر دو بیانی از یکدیگر هستند، این قضیه این نتیجه را می‌رساند که ماشین بوچی و ماشین قطعی مولر به‌طور مساوی بیانگر یکدیگر هستند.

بیان اصلی قضیه

در مقاله اصلی مک‌ناتون، قضیه بدین صورت بیان شده‌است که: " یک ω-رویداد منظم است اگر و فقط اگر حالت متناهی باشد."

امروزه از عبارت ω-زبان‌ها به جای ω-رویدادها استفاده می‌شود. همچنین طبق تعریف مک‌ناتون یک ω-رویداد، یک رویداد حالت متناهی است اگر یک ماشین مولر قطعی وجود داشته باشد که آن را تشخیص دهد.

ساختن یک زبان ω-منظم از یک ماشین مولر قطعی

اثبات یک طرف این قضیه بدین صورت است که نشان داده می‌شود هر ماشین مولر داده شده یک زبان ω-منظم را تشخیص می‌دهد. فرض کنید (A = (Q,Σ,δ,q₀,F یک ماشین قطعی مولر باشد. اتحاد تعداد زیاد و معینی از زبان‌های ω-منظم، یک زبان ω-منظم را تولید می‌کند، لذا بدون کم شدن از کلیت مساله می‌توان فرض نمود که شرط قبولی مولر F دقیقاً شامل یک مجموعه از حالت‌های {q₁,...,q_n} می‌شود. فرض می‌شود که α یک زبان منظم باشد که عناصرش A را از q₀ تا q₁ دربر بگیرد. برای هر i از 1 تا β_i ،n یک زبان منظمی باشد که عناصرش A را از q_i تا q_{(i mod n)+1} را بدون عبور از هر وضعیتی خارج از {q₁,...,q_n} در بر بگیرند. ادعا می‌شود که α(β_1...βn)^ω یک زبان ω-منظم است که توسط ماشین مولر A تشخیص داده می‌شود.

ساختن یک ماشین مولر قطعی از یک زبان ω-منظم داده شده

سمت دیگر قضیه را بدین طریق می‌توان اثبات کرد که به ازای هر زبان ω-منظم داده شده یک ماشین مولر وجود دارد که آن را تشخیص بدهد. اتحاد تعداد متناهی و زیادی از ماشین‌های قطعی مولر به سادگی قابل ساخت است، لذا بدون کم شدن از کلیت مساله، فرض می‌شود که زبان ω-منظم داده شده به شکل αβ^ω است. همچنین فرض شود که ω-کلمه w=a₁,a₂,... ∈ αβ^ω. w(i,j یک بخش معین شامل a_{i+1,...,aj-1,aj} از w در نظر گرفته می‌شود. برای ساختن ماشین مولر مرتبط با αβ^ω، دو مفهموم در رابطه با w معرفی می‌شود.
خدمت (به انگلیسی: Favor)
زمان j در خدمت زمان i است اگر j > i و *w(0,i) ∈ αβ و *w(i,j) ∈ β.
هم‌ارزی (به انگلیسی: Equivalence)
با ارزیابی در زمان i، k هم‌ارز است با j اگر *i,j≤k w(0,j) ∈ αβ*، w(0,i) ∈ αβ، و برای هر کلمه x در *w(i,k)x ∈ β*، Σ، اگر و فقط اگر *w(j,k)x ∈ β یا به عبارتی (E(i,j,k. به سادگی می‌توان توجه کرد که اگر (E(i,j,k آنگاه برای همه k <l داریم (E(i,j,l. به عبارت دیگر، اگر چنانچه i و j هم‌ارز ارزیابی شوند، در آن صورت از آن به بعد هم‌ارز خواهند ماند. همچنین برای مقدار l مشابه، l به i خدمت می‌کند اگر و فقط اگر l به j خدمت کند. قرار می‌دهیم (E(i,j اگر یک k وجود داشته باشد که (E(i,j,k.
فرض کنید که p تعداد وضعیت‌ها در کمترین ماشین متناهی معین A^β* باشد که زبان *β را تشخیص می‌دهد. اکنون به بیان دو لم دربارهٔ دو مفهوم بالا می‌پردازیم.
لم 1
برای هر زمانی چون k، در میان زمان‌های i و j که i,j<k به طوریکه (w(0,i و (*w(0,j ∈ αβ و تعداد هم‌ارزی‌های ایجاد شده توسط (E(i,j,k به وسیله p متناهی شده‌است.
لم 2
W ∈ αβ^ω اگر و فقط اگر زمانی چون i وجود داشته باشد که به تعداد نامتناهی زمان هم‌ارز با i باشد که به i خدمت کند.

ساختن ماشین مولر

هر دو مفهموم "خدمت کردن" و "هم‌ارزی" در لم 2 مورد استفاده قرار گرفته‌است. اکنون از این لم برای ساختن یک ماشین مولر برای زبان αβ^ω استفاده می‌کنیم. ماشین پیشنهادی یک کلمه را قبول می‌کند اگر و فقط اگر زمان i وجود داشته باشد که سمت راست لم 2 را ارضا گرداند. ماشین مذکور در ادامه توصیف شده‌است. توجه شود که این ماشین، یک ماشین قطعی مولر خواهد بود.
این ماشین شامل p+2 ماشین متناهی قطعی و یک کنترل‌کننده مستر (به انگلیسی: master controller) باشد که p سایز A^β* می‌باشد. یکی از p+2 ماشین قادر است تا *αβ را تشخیص دهد و این ماشین در هر چرخه ورودی می‌گیرد. در هر زمان i یا کنترل‌کننده مستر ارتباط برقرار می‌کند، خواه *w(0,i) ∈ αβ برقرار باشد و یا خیر. باقی این p+1 ماشین کپی‌هایی از A^β* هستند. مستر می‌تواند یک ماشین A^β* را فعال یا غیر فعال گرداند. اگر مستر آن را غیرفعال گرداند، آنگاه آن در حالت ابتدایی خود باقی مانده و نسبت به ورودی‌ها بی‌توجه خواهد شد. اگر مستر آن را فعال گرداند، سپس آن ماشین داده را خوانده و حرکت می‌کند تا زمانی که مستر آن را غیرفعال گردانیده و وادار به بازگشت به حالت ابتدایی کند. مستر قادر است تا یک ماشین A^β* را به تعداد دفعاتی که مایل است فعال و غیرفعال گرداند. مستر در هر لحظه اطلاعات زیر را دربارهٔ ماشین‌های A^β* ذخیره می‌کند.

• حالت‌های جاری ماشین‌های A^β*
• لیستی از ماشین‌های A^β* فعال به ترتیب زمان فعال‌سازیشان
• برای هر ماشین A^β* که فعال است، M، مجموعه ماشین‌های فعال دیگر که در زمان فعالسازی M، حالت پذیرش دارند. به عبارت دیگر، اگر یک ماشینی در زمان i فعال شده باشد و ماشین‌های دیگری در زمان j<i آخرین بار فعال شده باشند، و تا زمان i هم فعال بمانند، آنگاه مستر ثبت می‌کند که آیا i به j خدمت می‌کند یا خیر. این ثبتِ اطلاعات زمانی متوقف می‌شود که ماشین دیگری پیش از M غیر فعال گردد.
  

در ابتدا، مستر ممکن است با توجه به α به دو شکل متفاوت عمل کند. اگر α محتوی کلمات خالی باشد آنگاه تنها یکی از A^β* فعال خواهد بود، در غیر آن صورت، هیچ‌کدام از آن‌ها در شروع فعال نخواهند بود. بعدها در زمانی چون i، اگر *w(0,i) ∈ αβ و هیچکدام از ماشین‌های A^β* در حالت اولیه نباشند، آنگاه مستر یکی از ماشین‌های غیرفعال را فعال کرده و ماشینی که به تازگی فعال شده شروع به دریافت ورودی از زمان i+1 می‌کند. در زمانی دیگر، اگر دو ماشین A^β* به حالت یکسانی برسند، سپس مستر ماشینی را که دیرتر از دیگری فعال شده را غیرفعال می‌کند. توجه شود که مستر تصمیمات بالا را با توجه به اطلاعات ذخیره کرده اتخاذ می‌کند.
برای خروجی، مستر یک جفت چراغ سبز و قرمز را برای هر ماشین A^β* داراست.اگر یک ماشین به حالت غیرفعال برود، چراغ قرمز روشن می‌شود. چراغ سبز ماشین M که در زمان j فعال شده‌است در دو حالت زیر در زمان i روشن خواهد بود:

• M در حالت اولیه قرار دارد، در نتیجه (E(j,i,i و i به j خدمت می‌کند (حالت اولیه باید که حالت پذیرش باشد).
• برای ماشین دیگری چون M' که فعال است و در زمان k فعال شده‌است، که در آن j<k<i، داریم که k به j خدمت می‌کند (مستر اطلاعات ثبت شده را دارد) و i زودترین زمانی است که در آن (E(j,k,i (ماشین 'M در زمان i غیر فعال خواهد شد).
  

توجه داشته باشید که چراغ سبز برای ماشین M، هر سری که یک ماشین به سبب M غیرفعال می‌شود، روشن نمی‌شود.
لم 3
اگر یک زمان هم‌ارز برای تعداد نامتناهی از زمان‌ها وجود داشته باشد که به آن خدمت کنند و i زودهنگام‌ترین آن‌ها باشد، آنگاه یک ماشین A^β* مثل M در زمان i فعال می‌شود و برای همیشه فعال باقی می‌ماند (هیچ چراغ قرمزی روشن نمی‌شود پس ار آن) و چراغ سبز بینهایت بار میزند.
لم 4
برعکس، اگر ماشین A^β* مانند M وجود داشته باشد که چراغ سبزش بینهایت بار روشن شده بوده باشد و چراغ قرمزش تنها دفعات متناهی زده باشد، آنگاه زمان‌های نامتناهی وجود خواهد داشت که هم‌ارز بوده و به آخرین زمانی که ماشین M فعال شده‌است، خدمت می‌کند.
لم 5
w ∈ αβ^ω اگر و فقط اگر برای برخی ماشین‌های A^β* چراغ سبز تعداد دفعات نامتناهی فلاش زده و چراغ قرمز تنها دفعات متناهی فلاش می‌زند.
توصیف بالا از یک ماشین کامل می‌تواند به عنوان یک ماشین قطعی گسترده در نظر گرفته شود. اکنون باید شرط پذیرش مولر تعریف گردد. در این ماشین گسترده، μ_n را مجموعه حالت‌های مرتبط با ماشین nام از نوع A^β* تعریف می‌کنیم که در آن چراغ سبز فلاش زده و چراغ قرمز فلاش نمی‌زند. فرض کنید ν_n مجموعه حالت‌هایی باشد که در آن چراغ قرمز مربوط ماشین nام فلاش نمی‌زند. در نتیجه، شرط پذیرش مولر خواهد بود: {F = { S | ∃n μ_n ⊆ S ⊆ ν_n  این شرط، ساخت ماشین مولر مورد نظر را به اتمام می‌رساند.

جستارهای وابسته

• نظریه اتوماتا
• زبان منظم

منابع

• ویکی‌پدیای انگلیسی

• A. Saoudi, "Generalized automata on infinite trees and Muller-McNaughton's Theorem", [۱], France, April 1988
• Daniele Mundici, "A Constructive Proof of McNaughton's Theorem in Infinite-Valued Logic", Vol. 59, No. 2, 1994
• Bertrand Le Saec, Jean-Eric Pin,Pascal Weil, "A purely algebraic proof of McNaughton's theorem on infinite words", 2005