{"header":{"message":"More on quantelim.","description":null,"timestamp":"2022-01-04T18:30:43.350862364Z","authors":[{}]},"hash":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC","authors":[{"login":"finegeometer","key":"64ARLu9ao3fdRKWR644xoCX9eBBEMzfkyWsK7kYdkcxn"}],"deps":{"hashes":[["YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC","More on quantelim."],["AA",null],["SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC","Write a bit more about quantifier elimination."],["7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC","Create book. Write about using quantifier elimination for a graphing calculator."]],"deps":["SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC"],"known":["7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC"]},"hunks":[{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":28,"ins":{"up_context":[{"change":3,"pos":1144}],"down_context":[{"change":2,"pos":83}],"flag":"BLOCK","start":0,"end":161,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1144},"to":{"change":3,"start":1144,"end":1247},"introduced_by":3},{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1247},"to":{"change":2,"start":0,"end":83},"introduced_by":2}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"It would also be useful to have an operation like `something_satisfying : (number -> bool) -> number`, but it would require some thought to implement correctly.","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:160"}}],"del_contents":[{"Del":{"text":"It might also be useful to have an operation like `something_satisfying : (number -> bool) -> number`.","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1246"}},{"Del":{"text":"This should be possible, but it would require some thought to implement correctly.","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:82"}}]}},{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":35,"ins":{"up_context":[{"change":2,"pos":173}],"down_context":[{"change":2,"pos":260}],"flag":"BLOCK","start":162,"end":271,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":173},"to":{"change":2,"start":173,"end":260},"introduced_by":2}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"(<), (>), (<=), (>=) : number -> number -> bool","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:209"}},{"Add":{"text":"(=) : a -> a -> bool","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:230"}},{"Add":{"text":"(&&), (||), (=>) : bool -> bool -> bool","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:270"}}],"del_contents":[{"Del":{"text":"(=), (<), (>), (<=), (>=) : number -> number -> bool","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:225"}},{"Del":{"text":"(&&), (||) : bool -> bool -> bool","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:259"}}]}},{"Edit":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":40,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":304}],"down_context":[{"change":2,"pos":304}],"flag":"BLOCK","start":272,"end":364,"inode":{"change":3,"pos":18}}},"contents":[{"Add":{"text":"forall, exists : (number -> bool) -> bool","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:313"}},{"Add":{"text":"something_satisfying : (number -> bool) -> number","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:363"}}]}},{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":44,"ins":{"up_context":[{"change":3,"pos":1514}],"down_context":[{"change":2,"pos":335}],"flag":"BLOCK","start":365,"end":396,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1514},"to":{"change":2,"start":309,"end":335},"introduced_by":2}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"Some useful derived functions:","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:395"}}],"del_contents":[{"Del":{"text":"Useful derived functions:","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:334"}}]}},{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":46,"ins":{"up_context":[{"change":2,"pos":343}],"down_context":[{"change":2,"pos":578}],"flag":"BLOCK","start":397,"end":472,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":2,"pos":343},"to":{"change":2,"start":343,"end":578},"introduced_by":2}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"-- Useful for thickening lines, so they are actually visible on the graph.","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:471"}}],"del_contents":[{"Del":{"text":"{-","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:345"}},{"Del":{"text":" If you graph `x, y => y = x^2`, the result will be invisible, because it's an infinitely thin curve.","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:450"}},{"Del":{"text":" If you graph `holds_within 0.1 (x, y => y = x^2)`, the result will be a curve of width 0.2, so you can actually see it.","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:574"}},{"Del":{"text":"-}","pos":"SZCENJWWEDSFJJNNFSUG3SC2ATQLKYQFZ5YXSTOADLV3EIOP2KSAC:577"}}]}},{"Edit":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":50,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":740}],"down_context":[{"change":2,"pos":740}],"flag":"BLOCK","start":473,"end":897,"inode":{"change":3,"pos":18}}},"contents":[{"Add":{"text":"","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:473"}},{"Add":{"text":"abs : number -> number","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:496"}},{"Add":{"text":"abs x = if (x < 0) (-x) x","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:522"}},{"Add":{"text":"","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:523"}},{"Add":{"text":"-- The limit of f as its input goes to zero.","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:568"}},{"Add":{"text":"limit : (number -> number) -> number","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:605"}},{"Add":{"text":"limit x f = ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:618"}},{"Add":{"text":" something_satisfying (l -> ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:650"}},{"Add":{"text":" ∀ε. ε > 0 => ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:676"}},{"Add":{"text":" ∃δ. δ > 0 && ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:706"}},{"Add":{"text":" ∀x. abs x < δ => ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:743"}},{"Add":{"text":" abs (f x - l) < ε","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:782"}},{"Add":{"text":" )","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:788"}},{"Add":{"text":"","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:789"}},{"Add":{"text":"derivative : (number -> number) -> (number -> number)","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:843"}},{"Add":{"text":"derivative f x = limit (dx -> (f (x+dx) - f x) / dx)","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:896"}}]}},{"Edit":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":68,"atom":{"NewVertex":{"up_context":[{"change":2,"pos":745}],"down_context":[{"change":2,"pos":745}],"flag":"BLOCK","start":898,"end":979,"inode":{"change":3,"pos":18}}},"contents":[{"Add":{"text":"For efficiency reasons, limit should be implemented as a primitive, if possible.","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:978"}}]}},{"Edit":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":73,"atom":{"EdgeMap":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":1639},"to":{"change":3,"start":1639,"end":2411},"introduced_by":3}],"inode":{"change":3,"pos":18}}},"contents":[{"Del":{"text":"","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1639"}},{"Del":{"text":"If it were, trig functions could be defined like this:","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1694"}},{"Del":{"text":"\\\\[","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1698"}},{"Del":{"text":" \\\\begin{align*}","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1718"}},{"Del":{"text":" & \\\\exists \\\\sin. \\\\exists \\\\cos. \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1761"}},{"Del":{"text":" & \\\\quad \\\\cos 0 = 1 \\\\ \\\\land \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1801"}},{"Del":{"text":" & \\\\quad \\\\sin 0 = 0 \\\\ \\\\land \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1841"}},{"Del":{"text":" & \\\\quad (\\\\forall x. \\\\forall \\\\epsilon. \\\\epsilon > 0 \\\\implies \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1916"}},{"Del":{"text":" & \\\\qquad \\\\exists \\\\delta. \\\\delta > 0 \\\\ \\\\land \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:1975"}},{"Del":{"text":" & \\\\qquad \\\\quad \\\\forall y. |y - x| < \\\\delta \\\\implies \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2041"}},{"Del":{"text":" & \\\\qquad \\\\qquad |(\\\\sin y - \\\\sin x) / (y - x) - \\\\cos x| < \\\\epsilon \\\\ \\\\land \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2132"}},{"Del":{"text":" & \\\\qquad \\\\qquad |(\\\\cos y - \\\\cos x) / (y - x) + \\\\sin x| < \\\\epsilon \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2213"}},{"Del":{"text":" & \\\\quad ) \\\\ \\\\land \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2243"}},{"Del":{"text":" & \\\\quad \\\\textit{rest of expression} \\\\\\\\","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2290"}},{"Del":{"text":" & \\\\end{align*}","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2310"}},{"Del":{"text":"\\\\]","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2314"}},{"Del":{"text":"(Yes, I'm using the epsilon-delta definition of derivative to describe differential equations.)","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2410"}}]}},{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":74,"ins":{"up_context":[{"change":3,"pos":2412}],"down_context":[{"change":3,"pos":2609}],"flag":"BLOCK","start":980,"end":1289,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2412},"to":{"change":3,"start":2412,"end":2609},"introduced_by":3}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"If it were, the integers could be defined as follows:","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1033"}},{"Add":{"text":"```text","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1041"}},{"Add":{"text":"is_integer : number -> bool","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1069"}},{"Add":{"text":"is_integer n = ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1085"}},{"Add":{"text":" ∃sin. ∃cos. ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1106"}},{"Add":{"text":" cos 0 = 1 && sin 0 = 0 && ","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1141"}},{"Add":{"text":" derivative sin = cos && derivative cos = (x -> -sin x)) &&","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1208"}},{"Add":{"text":" ∃π. π > 3 && π < 4 && sin π = 0 &&","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1257"}},{"Add":{"text":" sin (π*n) = 0","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1284"}},{"Add":{"text":"```","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1288"}}],"del_contents":[{"Del":{"text":"If you have trig functions, you can define the natural numbers:","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2475"}},{"Del":{"text":"\\\\[\\\\text{is_natural}(x) = x \\\\geq 0 \\\\land \\\\exists \\\\pi. \\\\pi > 3 \\\\land \\\\pi < 4 \\\\land \\\\sin \\\\pi = 0 \\\\land \\\\sin \\\\pi x = 0\\\\]","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2608"}}]}},{"Replacement":{"inode":{"change":3,"pos":18},"path":"src/quant_elim.md","line":85,"ins":{"up_context":[{"change":3,"pos":2610}],"down_context":[{"change":3,"pos":2677}],"flag":"BLOCK","start":1290,"end":1359,"inode":{"change":3,"pos":18}},"del":{"edges":[{"previous":"BLOCK","flag":"BLOCK | DELETED","from":{"change":3,"pos":2610},"to":{"change":3,"start":2610,"end":2677},"introduced_by":3}],"inode":{"change":3,"pos":18}},"ins_contents":[{"Add":{"text":"And then you could use standard Godelian tricks to create a paradox.","pos":"YV2HUWPVYEGY6WH3C37ZPTXYULZZCG6CPUMAKZ767SFC623DMP3AC:1358"}}],"del_contents":[{"Del":{"text":"And then you can use standard Godelian tricks to create a paradox.","pos":"7HRLRQKVDELAMQDBRZJGKX3QCN3YBIZHZJAGMBPWJEIXIAIBZETQC:2676"}}]}}],"owner":"finegeometer","repo":"Ideas","token":"qj4oiEhay14dd3WEzUgnITSz6BTIT2FZLTOs3/N7v9A=","login":null}

…

Dependencies

Change contents

Review