الگوریتم روش کاهش در درستی نگارش فرمول در منطق گزاره‌ها

کد پایتون الگوریتم تصمیم‌پذیری نگارش فرمول در زیر آمده است. این کد را می‌توانید با کلیک کردن کپی کنید.

تعریب زبان، وازگان و رابط‌ها

import re # Regular expressions :درخواست برای کتابخوانه
CONNECTIVES = ['⊃', '∧', '∨', '~']
BINARY_CONNECTIVES = ['⊃', '∧', '∨']
CONNECTIVE_MAPPING = {
    '>': '⊃',
    '&': '∧',
    '|': '∨',
}

جایگزینی رابط‌های ['>', '&', '|'] به رابط‌های استاندارد'z'.

def _standardize_connectives(formula_str):
    for ascii_char, unicode_char in CONNECTIVE_MAPPING.items():
        formula_str = formula_str.replace(ascii_char, unicode_char)
    return formula_str

جایگزینی اتم‌ها به 'z'.

def _f1_replace_atoms(sub_formula_str, new_atom_char='z'):
    result = []
    for char in sub_formula_str:
        """ بررسی به قاعده بودن نویسه‌های"""
        if 'a' <= char <= 'z' and char != new_atom_char and char not in CONNECTIVES:
            result.append(new_atom_char)
        else:
            result.append(char)
    return "".join(result)

کاهش '~z' به '(z)' و 'z' به 'z':

def _f2_negation_and_parens(sub_formula_str):
    s = sub_formula_str.replace("~z", "z")
    ss = s.replace("(z)", "z")
    return ss

کاهش (z γ z) به 'z' [یا z γ z به 'z' برای وقتی که پرانتز نباشد، یعنی تمام رشته است.] (نماد γ یک رابط دوتایی است.)

def _f3_binary_reduction(sub_formula_str):
    
    escaped_binary_connectives = '|'.join(re.escape(c) for c in BINARY_CONNECTIVES)
    parenthesized_pattern = re.compile(r"\(z\s*(" + escaped_binary_connectives + r")\s*z\)")
    
    match = parenthesized_pattern.search(sub_formula_str)
    if match:
        start_index = match.start()
        end_index = match.end()
        return sub_formula_str[:start_index] + 'z' + sub_formula_str[end_index:]
    """ اگر مطابقت پرانتزی وجود ندارد
              z γ z
     مورد جستجو قرار می‌گیرد """
    bare_pattern = re.compile(r"^z\s*(" + escaped_binary_connectives + r")\s*z$")
    bare_match = bare_pattern.search(sub_formula_str)
    if bare_match:
        return 'z'

    return sub_formula_str """ کاهش بیشتر میسر نیست"""
    

با کاهش یک فرمول در منطق گزاره‌ای به 'z'، «صحت نحوی» آن معین می‌شود. در صورت صحت، مقدار True و در غیر این صورت مقدار False برگردانده می‌شود.

def formula_reduction_algorithms(formula):
    z_atom = 'z'

    # Step 0: استاندارد سازی رابط‌های ورودی
    standardized_formula = _standardize_connectives(formula)

    # Step 1: A1 = f1(standardized_formula)
    A1 = _f1_replace_atoms(standardized_formula, z_atom)

    # Step 2: A2 = f2(A1)
    A2 = _f2_negation_and_parens(A1)

    # Step 3    چرخه کاهش، یعنی کارزدن  
    #           F4 
    #           تا پابرجایی 
    current_formula_state = A2 
    MAX_ITERATIONS = 1000 """ حداکثر مجاز تعداد دور در چرخه:  
    نقطه خروج برای مانع شدن از دورهای‌ بی‌پایان"""
    for _ in range(MAX_ITERATIONS): 
        next_formula_state = _f4_combined_reduction(current_formula_state)
        if next_formula_state == current_formula_state:
            """ بررسی پابرجایی، یعنی اگر حالت بعد با حالت قبل مساوی است"""
            return current_formula_state == z_atom
        current_formula_state = next_formula_state
    
    """ اگر چرخه پیش از رسیدن به حداکثر دور مجاز پایان یافته است"""
    return False """ فرمول صحت نحوی ندارد"""
    

اجرا و آزمون

if __name__ == "__main__":
    print(f"'(p & q) > r' is correct: \
	 {formula_reduction_algorithms('(p & q) > r')}")
    print(f"'(p & q) > (~r)' is correct:\
	 {formula_reduction_algorithms('(p & q) > (~r)')}")