Pytania otagowane jako term-rewriting

Załóżmy, że mamy prosty język, który składa się z terminów: truetrue\mathtt{true} falsefalse\mathtt{false} jeśli są warunkami, to podobnie jest zi ft1,t2,t3t1,t2,t3t_1,t_2,t_3ift1thent2elset3ift1thent2elset3\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 Załóżmy teraz następujące logiczne reguły oceny: iftruethent2elset3→t2[E-IfTrue]iffalsethent2elset3→t3[E-IfFalse]t1→t′1ift1thent2elset3→ift′1thent2elset3[E-If]iftruethent2elset3→t2[E-IfTrue]iffalsethent2elset3→t3[E-IfFalse]t1→t1′ift1thent2elset3→ift1′thent2elset3[E-If] \begin{gather*} \dfrac{} {\mathtt{if}\: \mathtt{true} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_2} \text{[E-IfTrue]} \quad \dfrac{} {\mathtt{if}\: \mathtt{false} \:\mathtt{then}\: t_2 \:\mathtt{else}\: …

14 logic  semantics  proof-techniques  term-rewriting 

Zrobiłem trochę googleingu i podszedłem trochę za krótko. Zastanawiam się, jakie są główne powody dla naukowców zajmujących się obliczeniami, programistów, aby studiować przepisywanie terminów i / lub przepisywanie grafów terminowych. O ile mogę stwierdzić, pomaga to w podstawowym rozumowaniu programów funkcjonalnych i (imperatywnej) kontroli programów. Najwyraźniej jest to temat bardzo …

12 term-rewriting 

Przepisanie systemu jest zestaw reguł w postaci . Jeśli zastosujemy tę regułę do łańcucha , zastąpimy dowolny podciąg in podciągiem i odwrotnie.A↔BA↔BA \leftrightarrow BwwwAAAwwwBBB Biorąc pod uwagę początkowy ciąg możemy wyprowadzić w systemie według następujących reguł:AAABBAAABBAAABBBAABBAABBAAB A↔BAA↔BAA \leftrightarrow BA BABA↔AABBBABA↔AABBBABA \leftrightarrow AABB AAA↔ABAAA↔ABAAA \leftrightarrow AB BA↔ABBA↔ABBA \leftrightarrow AB Czy jest …

11 computability  term-rewriting 

Niech →β→β\to_\beta będzie redukcją ββ\beta w rachunku λλ\lambda . Zdefiniuj ββ\beta rozszerzenie ←β←β\leftarrow_\beta przez t′←βt⟺t→βt′t′←βt⟺t→βt′t'\leftarrow_\beta t \iff t\to_\beta t' . Czy ←β←β\leftarrow_\beta zbieżny? Innymi słowy, nie mamy, że dla każdego l,d,rl,d,rl,d,r , jeżeli l→∗βd←∗βrl→β∗d←β∗rl \to_\beta^* d\leftarrow_\beta^* r , to istnieje uuu taki sposób, że l←∗βu→∗βrl←β∗u→β∗rl\leftarrow_\beta^* u \to_\beta^* r ? Słowa …

10 lambda-calculus  term-rewriting