Nest abstract rewriting systems under formal systems.

c-declarations
Joshua Potter 2024-07-21 06:54:03 -06:00
parent 6ba651c41b
commit b9504d7857
3 changed files with 37 additions and 48 deletions

View File

@ -620,7 +620,7 @@
"_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932", "_journal/2024-07/2024-07-18.md": "237918b58424435959cbc949d01e7932",
"_journal/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3", "_journal/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3",
"_journal/2024-07/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc", "_journal/2024-07/2024-07-19.md": "e9fe4569f88e1ba9393292bcf092edfc",
"_journal/2024-07-21.md": "682ee0ada782dd281d8fd217227e985c", "_journal/2024-07-21.md": "dd5dd93f119f69571a78e027fab7da5d",
"_journal/2024-07/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3", "_journal/2024-07/2024-07-20.md": "d8685729effc374e4ece1e618c2fdad3",
"logic/classical/index.md": "ee0a4b2bfcfa2cab0880db449cb62df1", "logic/classical/index.md": "ee0a4b2bfcfa2cab0880db449cb62df1",
"logic/classical/truth-tables.md": "b739e2824a4a5c26ac446e7c15ce02aa", "logic/classical/truth-tables.md": "b739e2824a4a5c26ac446e7c15ce02aa",
@ -630,7 +630,8 @@
"formal-system/logical-system/pred-logic.md": "2524ccc09561bc219dab3f32010a0161", "formal-system/logical-system/pred-logic.md": "2524ccc09561bc219dab3f32010a0161",
"formal-system/logical-system/prop-logic.md": "b61ce051795d5a951c763b928ec5cea8", "formal-system/logical-system/prop-logic.md": "b61ce051795d5a951c763b928ec5cea8",
"formal-system/index.md": "3d31c99bffdcb05de9f2e32ac6319952", "formal-system/index.md": "3d31c99bffdcb05de9f2e32ac6319952",
"programming/short-circuit.md": "c256ced42dc3b493aff5a356e5383b6e" "programming/short-circuit.md": "c256ced42dc3b493aff5a356e5383b6e",
"formal-system/abstract-rewriting.md": "8424314a627851c5b94be6163f64ba30"
}, },
"fields_dict": { "fields_dict": {
"Basic": [ "Basic": [

View File

@ -1,44 +0,0 @@
---
title: Normal Form
TARGET DECK: Obsidian::STEM
FILE TAGS: ars::normal
tags:
- ars
---
## Overview
An object is said to be in **normal form** if it cannot be reduced any further. Examples of normal form include:
* [[truth-tables|Conjunctive Normal Form]]
* [[truth-tables|Disjunctive Normal Form]]
* [[pred-logic#Identifiers|Prenex Normal Form]]
* [[beta-reduction#Normal Form|β-normal forms]]
%%ANKI
Basic
What does it mean for an object to be in normal form?
Back: It cannot be rewritten/reduced any further.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675146194-->
END%%
%%ANKI
Basic
What zero-order logical normal form(s) have only $\land$ and $\lor$ operators?
Back: CNF and DNF.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675369145-->
END%%
%%ANKI
Basic
What first-order logical normal form(s) writes bound identifiers before free ones?
Back: PNF
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675369187-->
END%%
## Bibliography
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.

View File

@ -1,15 +1,23 @@
--- ---
title: Abstract Rewriting Systems title: Abstract Rewriting Systems
TARGET DECK: Obsidian::STEM TARGET DECK: Obsidian::STEM
FILE TAGS: ars FILE TAGS: formal-system::abstract-rewriting
tags: tags:
- ars - abstract-rewriting
- formal-system
--- ---
## Overview ## Overview
In an **abstract rewriting system** (ARS), an object is said to be in **normal form** if it cannot be rewritten any further, i.e. it is irreducible. An object is said to be in **canonical form** if it is presented in the "standard" representation (where "standard" is defined per field). In an **abstract rewriting system** (ARS), an object is said to be in **normal form** if it cannot be rewritten any further, i.e. it is irreducible. An object is said to be in **canonical form** if it is presented in the "standard" representation (where "standard" is defined per field).
Examples of normal form include:
* [[truth-tables|Conjunctive Normal Form]]
* [[truth-tables|Disjunctive Normal Form]]
* [[pred-logic#Identifiers|Prenex Normal Form]]
* [[beta-reduction#Normal Form|β-normal forms]]
In most fields, a canoncial form specifies a *unique* representation. In most fields, a canoncial form specifies a *unique* representation.
%%ANKI %%ANKI
@ -59,6 +67,30 @@ Reference: “Canonical Form,” in _Wikipedia_, January 7, 2024, [https://en.wi
<!--ID: 1719067812833--> <!--ID: 1719067812833-->
END%% END%%
%%ANKI
Basic
What does it mean for an object to be in normal form?
Back: It cannot be rewritten/reduced any further.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675146194-->
END%%
%%ANKI
Basic
What zero-order logical normal form(s) have only $\land$ and $\lor$ operators?
Back: CNF and DNF.
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675369145-->
END%%
%%ANKI
Basic
What first-order logical normal form(s) writes bound identifiers before free ones?
Back: PNF
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
<!--ID: 1707675369187-->
END%%
## Confluence ## Confluence
**Confluence** is the property by which two different terms can be further reduced to one common term. That is to say, confluence is a property of rewriting systems describing which terms in such a system can be rewritten in more than one way. **Confluence** is the property by which two different terms can be further reduced to one common term. That is to say, confluence is a property of rewriting systems describing which terms in such a system can be rewritten in more than one way.