Notes on normal forms.
parent
6b6d109da7
commit
99e807f807
|
@ -98,7 +98,7 @@
|
|||
"logic/index.md": "3084b41fe1451259a0cf3e54560c2e85",
|
||||
"logic/propositional.md": "e7dbb24674336beb44dc9ef4c9ae51ff",
|
||||
"lua/index.md": "26632dae1f852519e2f1af11d65c34eb",
|
||||
"nix/callPackage.md": "59796c480e2856fa7491f62ceb7e3c9c",
|
||||
"nix/callPackage.md": "140a02e57cd01d646483e3c21d72243d",
|
||||
"nix/index.md": "dd5ddd19e95d9bdbe020c68974d77a33",
|
||||
"posix/index.md": "f7b1ae55f8f5e8f50f89738b1aca9111",
|
||||
"posix/signals.md": "2120ddd933fc0d57abb93c33f639afd8",
|
||||
|
@ -119,16 +119,16 @@
|
|||
"algorithms/loop-invariants.md": "cbefc346842c21a6cce5c5edce451eb2",
|
||||
"algorithms/loop-invariant.md": "d883dfc997ee28a7a1e24b995377792b",
|
||||
"algorithms/running-time.md": "5efc0791097d2c996f931c9046c95f65",
|
||||
"algorithms/order-growth.md": "6e0f9e751eab24d74652851454264008",
|
||||
"algorithms/order-growth.md": "ac89d74204040a7c9b870e865c62aa59",
|
||||
"_journal/2024-02-08.md": "19092bdfe378f31e2774f20d6afbfbac",
|
||||
"algorithms/sorting/selection-sort.md": "73a077a726afd376650d1bd9e2d0bed9",
|
||||
"algorithms/index 1.md": "6fada1f3d5d3af64687719eb465a5b97",
|
||||
"binary/hexadecimal.md": "531ebb4b1b10a0ac60899164bc1c3f07",
|
||||
"binary/hexadecimal.md": "813512cb38700a8cb8ecf8ee9d6c9343",
|
||||
"binary/index.md": "a67b5d0c8ac53e076590f315cce22201",
|
||||
"_journal/2024-02-09.md": "a798d35f0b2bd1da130f7ac766166109",
|
||||
"c/types.md": "cf3e66e5aee58a94db3fdf0783908555",
|
||||
"logic/quantification.md": "b7cf646a8c33aa83f48ddc37c733fafb",
|
||||
"c/declarations.md": "6d80eca97506fae9a4a209a558d3aa84",
|
||||
"logic/quantification.md": "37655276de8da531ca2b12706a639224",
|
||||
"c/declarations.md": "ed6ed90493215546b4b181933e0d6004",
|
||||
"algorithms/sorting/bubble-sort.md": "16dad1016dc6555163e42ba20f1d152d",
|
||||
"_journal/2024-02-10.md": "562b01f60ea36a3c78181e39b1c02b9f",
|
||||
"_journal/2024-01/2024-01-31.md": "7c7fbfccabc316f9e676826bf8dfe970",
|
||||
|
@ -142,8 +142,9 @@
|
|||
"_journal/2024-02/2024-02-02.md": "a3b222daee8a50bce4cbac699efc7180",
|
||||
"_journal/2024-02/2024-02-01.md": "3aa232387d2dc662384976fd116888eb",
|
||||
"_journal/2024-02/2024-02-10.md": "562b01f60ea36a3c78181e39b1c02b9f",
|
||||
"_journal/2024-02-11.md": "438455de19ee8c76acce50a723612698",
|
||||
"binary/endianness.md": "d73bf4e10385cdbc672d40a53f0fe868"
|
||||
"_journal/2024-02-11.md": "afee9f502b61e17de231cf2f824fbb32",
|
||||
"binary/endianness.md": "29c0aea671aa25aead580e9431aba8cc",
|
||||
"logic/normal-form.md": "d6a79aa850e9830def15e9012a774057"
|
||||
},
|
||||
"fields_dict": {
|
||||
"Basic": [
|
||||
|
|
|
@ -11,3 +11,4 @@ title: "2024-02-11"
|
|||
- [ ] Log Work Hours (Max 3 hours)
|
||||
|
||||
* Notes on endianness.
|
||||
* Notes on prenex normal form and normal forms in general.
|
|
@ -91,6 +91,6 @@ Reference: Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambri
|
|||
<!--ID: 1707344177515-->
|
||||
END%%
|
||||
|
||||
## Reference
|
||||
## References
|
||||
|
||||
* Thomas H. Cormen et al., *Introduction to Algorithms*, 3rd ed (Cambridge, Mass: MIT Press, 2009).
|
|
@ -114,6 +114,6 @@ int main() {
|
|||
|
||||
The above snippet can be used to check endianness on the current machine. If big-endian, the output should be `01 23 45 67`. If little-endian, `67 45 23 01`.
|
||||
|
||||
## Reference
|
||||
## References
|
||||
|
||||
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
|
@ -222,6 +222,6 @@ Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Program
|
|||
<!--ID: 1707432641596-->
|
||||
END%%
|
||||
|
||||
## Reference
|
||||
## References
|
||||
|
||||
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
||||
|
|
|
@ -164,6 +164,6 @@ Reference: Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Program
|
|||
<!--ID: 1707493017246-->
|
||||
END%%
|
||||
|
||||
## Reference
|
||||
## References
|
||||
|
||||
* Bryant, Randal E., and David O'Hallaron. *Computer Systems: A Programmer's Perspective*. Third edition, Global edition. Always Learning. Pearson, 2016.
|
|
@ -0,0 +1,43 @@
|
|||
---
|
||||
title: Normal Form
|
||||
TARGET DECK: Obsidian::STEM
|
||||
FILE TAGS: logic
|
||||
tags:
|
||||
- logic
|
||||
---
|
||||
|
||||
## Overview
|
||||
|
||||
An object is said to be in **normal form** if it cannot be reduced any further. Examples of normal form include:
|
||||
|
||||
* [[equiv-trans#Normal Forms|Conjunctive Normal Form]]
|
||||
* [[equiv-trans#Normal Forms|Disjunctive Normal Form]]
|
||||
* [[quantification#Identifiers|Prenex Normal Form]]
|
||||
|
||||
%%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%%
|
||||
|
||||
## References
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
|
@ -9,7 +9,25 @@ tags:
|
|||
|
||||
## Overview
|
||||
|
||||
* **Existential quantification** asserts the existence of a member in a set (denoted the **range**) satisfying a property. There may be multiple members that satisfy the property; so long as one does, the existential quantification is considered true.
|
||||
A **quantifier** refers to an operator that specifies how many members of a set satisfy some formula. The most common quantifiers are $\exists$ and $\forall$, though others (such as the counting quantifier) are also used.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What are the most common first-order logic quantifiers?
|
||||
Back: $\exists$ and $\forall$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796763-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What term refers to operators like $\exists$ and $\forall$?
|
||||
Back: Quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796766-->
|
||||
END%%
|
||||
|
||||
* **Existential quantification** ($\exists$) asserts the existence of at least one member in a set satisfying a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
@ -43,7 +61,7 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707494819970-->
|
||||
END%%
|
||||
|
||||
* **Universal quantification** asserts that every member of a set satisfies a property.
|
||||
* **Universal quantification** ($\forall$) asserts that every member of a set satisfies a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
|
@ -98,11 +116,11 @@ Back: $\neg \forall x : S, \neg P(x)$
|
|||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
END%%
|
||||
|
||||
* **Counting quantification** asserts that a number of members of a set satisfy a property.
|
||||
* **Counting quantification** ($\exists^{=k}$ or $\exists^{\geq k}$) asserts that (at least) $k$ (say) members of a set satisfy a property.
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of exactly $k$ members)?
|
||||
What symbol denotes counting quantification (of *exactly* $k$ members)?
|
||||
Back: $\exists^{=k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819983-->
|
||||
|
@ -110,7 +128,7 @@ END%%
|
|||
|
||||
%%ANKI
|
||||
Basic
|
||||
What symbol denotes counting quantification (of at least $k$ members)?
|
||||
What symbol denotes counting quantification (of *at least* $k$ members)?
|
||||
Back: $\exists^{\geq k}$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707494819985-->
|
||||
|
@ -132,6 +150,81 @@ Reference: Gries, David. *The Science of Programming*. Texts and Monographs in
|
|||
<!--ID: 1707494832058-->
|
||||
END%%
|
||||
|
||||
## Reference
|
||||
## Identifiers
|
||||
|
||||
Identifiers are said to be **bound** if they are parameters to a quantifier. Identifiers that are not bound are said to be **free**. A first-order logic formula is said to be in **prenex normal form** (PNF) if written in two parts: the first consisting of quantifiers and bound variables (the **prefix**), and the second consisting of no quantifiers (the **matrix**).
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When is an identifier said to be bound?
|
||||
Back: When it is specified as a parameter to a quantifier.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796768-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
When is an identifier said to be free?
|
||||
Back: When it isn't specified as a parameter to a quantifier.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796770-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Cloze
|
||||
An identifier that is not {bound} is instead {free}.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796772-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Prenex normal form consists of what two parts?
|
||||
Back: The prefix and the matrix.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796773-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the prefix of a formula in PNF formatted?
|
||||
Back: As only quantifiers and bound variables.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796775-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the matrix of a formula in PNF formatted?
|
||||
Back: Without quantifiers.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796776-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are bound? $$\exists x, P(x) \land P(y)$$
|
||||
Back: Just $x$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796777-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
Which identifiers in the following are free? $$\exists x, P(x) \land P(y)$$
|
||||
Back: Just $y$.
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707674796779-->
|
||||
END%%
|
||||
|
||||
%%ANKI
|
||||
Basic
|
||||
How is the following rewritten in PNF? $$(\exists x, P(x)) \land (\exists y, P(y))$$
|
||||
Back: $\exists x \;y, P(x) \land P(y)$
|
||||
Reference: Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
||||
<!--ID: 1707675399517-->
|
||||
END%%
|
||||
|
||||
## References
|
||||
|
||||
* Gries, David. *The Science of Programming*. Texts and Monographs in Computer Science. New York: Springer-Verlag, 1981.
|
|
@ -111,6 +111,6 @@ Reference: Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https
|
|||
<!--ID: 1706828225240-->
|
||||
END%%
|
||||
|
||||
## Reference
|
||||
## References
|
||||
|
||||
* Yin, Ryan. “NixOS and Flakes Book.” Nix, February 1, 2024. [https://github.com/ryan4yin/nixos-and-flakes-book](https://github.com/ryan4yin/nixos-and-flakes-book)
|
||||
|
|
Loading…
Reference in New Issue