與傳遞閉包（可達性和生產率非終端）更換遞歸

有時候，當我想在合金使用遞歸，我發現我可以傳遞閉包，或序列度日。與傳遞閉包（可達性和生產率非終端）更換遞歸

例如，在上下文無關文法的模型：

abstract sig Symbol {} 
sig NT, T extends Symbol {} 

// A grammar is a tuple(V, Sigma, Rules, Start) 
one sig Grammar { 
    V : set NT, 
    Sigma : set T, 
    Rules : set Prod, 
    Start : one V 
} 

// A production rule has a left-hand side 
// and a right-hand side 
sig Prod { 
    lhs : NT, 
    rhs : seq Symbol 
} 

fact tidy_world { 
    // Don't fill the model with irrelevancies 
    Prod in Grammar.Rules 
    Symbol in (Grammar.V + Grammar.Sigma) 
}

可達非終端的一個可能的定義是「開始符號，以及任何非末端出現在右手側一個可達符號的規則。「一個簡單的翻譯將是

// A non-terminal 'refers' to non-terminals 
// in the right-hand sides of its rules 
pred refers[n1, n2 : NT] { 
    let r = (Grammar.Rules & lhs.n1) | 
    n2 in r.rhs.elems 
} 

pred reachable[n : NT] { 
    n in Grammar.Start 
    or some n2 : NT 
    | (reachable[n2] and refers[n2,n]) 
}

可以預見，這打擊了堆棧。但是，如果我們簡單地採取Grammar.Start的傳遞閉包下refers關係（或者，嚴格地說，從refers謂詞形成的關係），我們可以定義可訪問性：

// A non-terminal is 'reachable' if it's the 
// start symbol or if it is referred to by 
// (rules for) a reachable symbol. 
pred Reachable[n : NT] { 
    n in Grammar.Start.*(
    {n1, n2 : NT | refers[n1,n2]} 
) 
} 

pred some_unreachable { 
    some n : (NT - Grammar.Start) 
    | not Reachable[n] 
} 
run some_unreachable for 4

原則，生產性的定義符號同樣是遞歸的：符號是有生產力的，如果它是終端符號，或者它至少有一個規則，右邊的每個符號都是有生產力的。寫這個頭腦簡單的辦法就是

pred productive[s : Symbol] { 
    s in T 
    or some p : (lhs.s) | 
     all r : (p.rhs.elems) | productive[r] 
}

像可達性的簡單定義，這吹堆棧。但是我還沒有找到可以在符號上定義的關係，通過傳遞閉包，我可以得到我想要的結果。我發現了傳遞閉包不能代替遞歸的情況嗎？還是我沒有足夠努力去找到正確的關係？

有一個明顯的，如果費力，黑客：

pred p0[s : Symbol] { s in T } 
pred p1[s : Symbol] { p0[s] 
    or some p : (lhs.s) 
    | all e : p.rhs.elems 
    | p0[e]} 
pred p2[s : Symbol] { p1[s] 
    or some p : (lhs.s) 
    | all e : p.rhs.elems 
    | p1[e]} 
pred p3[s : Symbol] { p2[s] 
    or some p : (lhs.s) 
    | all e : p.rhs.elems 
    | p2[e]} 
... etc ... 
pred productive[n : NT] { 
    p5[n] 
}

該工程確定，只要一不忘記補充足夠的謂詞來處理非終端的引用可能的最長鏈，如果提高了範圍。

具體來說，我似乎有幾個問題;回答任何人都會受到歡迎：

1有沒有辦法來定義集生產合金非終端而不訴諸P0，P1，P2，...破解？

2如果一個人不得不求助於黑客，有沒有更好的方式來界定呢？

3作爲理論問題：是否有可能以表徵一組可使用的傳遞閉包來定義遞歸謂詞，或原子的序列，而不是遞歸？

來源

2016-01-27 C. M. Sperberg-McQueen

我發現了傳遞閉包不能代替遞歸的情況嗎？

是的，是這樣的。更確切地說，你發現了一個遞歸關係，它不能用一階傳遞閉包（在Alloy中支持）來表示。

有沒有辦法在合金中定義一組生產性非終端而不訴諸p0，p1，p2，... hack？如果不得不求助於黑客，有沒有更好的方法來定義它？

在Alloy中沒有辦法做到這一點。但是，在Alloy*中可能有一種方法可以支持更高階的量化。（這個想法是用一個關於「生產力」關係的生產要素集合來描述，這個生產要素集合將使用對生產符號集合的二階量化，並將這個集合約束爲最小。「A.1.9 Axiomatizing傳遞閉包」中的合金書）

作爲理論問題：是能夠表徵一組可使用的傳遞閉包來定義遞歸謂詞，或原子的序列，而不是遞歸？

這是一個有趣的問題。 wiki文章提到傳遞閉包和定點運算符被添加時（後者可以表達遞歸形式）提到二階邏輯的相對錶達性。

來源

2016-04-21 06:07:31 ivcha

與傳遞閉包（可達性和生產率非終端）更換遞歸

回答

相關問題