{
localUrl: '../page/order_monotone_examples.html',
arbitalUrl: 'https://arbital.com/p/order_monotone_examples',
rawJsonUrl: '../raw/5lf.json',
likeableId: '0',
likeableType: 'page',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
pageId: 'order_monotone_examples',
edit: '14',
editSummary: '',
prevEdit: '13',
currentEdit: '14',
wasPublished: 'true',
type: 'wiki',
title: 'Monotone function: examples',
clickbait: '',
textLength: '5910',
alias: 'order_monotone_examples',
externalUrl: '',
sortChildrenBy: 'likes',
hasVote: 'false',
voteType: '',
votesAnonymous: 'false',
editCreatorId: 'KevinClancy',
editCreatedAt: '2016-12-03 23:54:32',
pageCreatorId: 'KevinClancy',
pageCreatedAt: '2016-07-26 00:43:58',
seeDomainId: '0',
editDomainId: 'AlexeiAndreev',
submitToDomainId: '0',
isAutosave: 'false',
isSnapshot: 'false',
isLiveEdit: 'true',
isMinorEdit: 'false',
indirectTeacher: 'false',
todoCount: '0',
isEditorComment: 'false',
isApprovedComment: 'true',
isResolved: 'false',
snapshotText: '',
anchorContext: '',
anchorText: '',
anchorOffset: '0',
mergedInto: '',
isDeleted: 'false',
viewCount: '31',
text: 'Here are some examples of monotone functions.\n\nA cunning plan\n--------\n\nThere's a two-player game called 10 questions, in which player A begins the game by stating "I'm thinking of an X", where X can be replaced with any noun of player A's choosing.\n\nThen player B asks player A a series of questions, which player A must answer with either truthfully with "yes" or "no". After asking 10 questions, player B is forced to guess what the object player A was thinking of. Player B wins if the guess is correct, and loses otherwise. Player B may guess before 10 turns have expired, in which case the guess counts as one of\ntheir questions.\n\nHere is an example of a game of 10 questions:\n\nA: I'm thinking of a food.\n\nQuestion 1. \nB: Is it healthy? \nA: Yes.\n\nQuestion 2.\nB: Is it crunchy? \nA: No.\n\nQuestion 3.\nB: Must it be prepared before it is eaten?\nA: No.\n\nQuestion 4.\nB: Is yellow? \nA: Yes.\n\nQuestion 5.\nB: Is it a banana? \nA: Yes.\n\n**Player B wins**\n\nNow suppose that you are playing 10 questions as player B. Player A begins by stating\n"I'm thinking of a letter of the alphabet." You immediately think of a strategy\nthat requires no more than 5 guesses: repeatedly ask "does it come after $\\star$?"\nwhere $\\star$ is near the middle of the contiguous sequence of letters that you have\nnot yet eliminated. Initially the contiguous sequence of letters between A and Z\nhave not been eliminated.\n\n \nQuestion 1.\n*You:* Does it come after M?\n*Player A:* Yes.\n\nAt this point, the contiguous sequence of 13 letters that have not been eliminated is N-Z,\ninclusive.\n\nQuestion 2.\n*You:* Does it come after S? *Player A:* No.\n\nAt this point, the contiguous sequence of 6 letters that have not been eliminated is N-S,\ninclusive.\n\nQuestion 3. *You:* Does it come after P? *Player A:* Yes.\n\nWe've now narrowed it down to Q,R,and S.\n\nQuestion 4. *You:* Does it come after R? *Player A:* No.\n\nQuestion 5. *You:* Does it come after Q? *Player A:* No.\n\n*You:* Is it Q? *Player A:* Yes.\n\n**You win**\n\nBut what does this have to do with monotone functions? The letters of the alphabet form a poset $Alph = \\langle \\{A,...,Z\\}, \\leq_{Alph} \\rangle$ (in fact, a [540 totally ordered set]) under the standard alphabetic order. Your strategy for playing 10 questions can be viewed as probing a monotone function from $Alph$ to the 2-element poset **2** of a [57f boolean values], where $false <_{\\textbf{2}} true$. Specifically, the probed function $f : Alph \\to \\textbf{2}$ is defined such that $f(\\star) \\doteq Q >_{Alph} \\star$ \n\nThe monotonicity of $f$ is crucial to being able to eliminate possibilities at each step. If we probe $f$ at a letter $\\star_1$ and observe a false result, then any letter $\\star_2$ less than $\\star_1$ must map to false as well: $\\star_2 \\leq_{Alph} \\star_1$ implies $f(\\star_2) \\leq_{\\textbf{2}} f(\\star_1)$. Yes, we can demonstrate the aformentioned monotone function with a diagram, but since its size is unwieldy, it has been placed in the following hidden text block.\n\n%%hidden(Show solution):\n\n%%\n\n\n\n\nDeduction systems\n---------------\n\n[deduction_systems] allow one to infer new judgments from a set of known judgments. They are often specified as a set of rules, in which each rule is represented as a horizontal bar with one or more premises appearing above the bar and a conclusion that can be deduced from those premises appearing below the bar. \n\n\n\nThe above rules form a fragment of [57f propositional logic]. $\\phi$ and $\\psi$ are used to denote logical statements, called *propositions*. $\\wedge$ and $\\to$ are binary logical operators, each of which maps a pair of propositions to a single proposition. $\\wedge$ is the *and* operator: if $\\phi$ and $\\psi$ are logical statements, then $\\phi \\wedge \\psi$ is the simultaneous assertion of both $\\phi$ and $\\psi$. $\\to$ is the *implication* operator: $\\phi \\to \\psi$ asserts that if we know $\\phi$ to be true, then we can conclude $\\psi$ is true as well.\n\nThe leftmost rule has two premises $\\phi$ and $\\psi$, and concludes from these premises the proposition $\\phi \\wedge \\psi$. Invoking a rule to deduce its conclusion from its premises is called *applying* the rule. A tree of rule applications is called a [proof proof].\n\nDeduction systems are often viewed as proof languages. However, it can also be fruitful to view a deduction system as a function which, given a set of input propositions, produces the set of all propositions that can be concluded from exactly one rule application, using the input propositions as premises. More concretely, letting $X$ be the set of propositions, the above set of deduction rules corresponds to the following function $F : \\mathcal P(X) \\to \\mathcal P(X)$.\n\n$F(A) = \\\\ ~~ \\{ \\phi \\wedge \\psi\\mid\\phi \\in A, \\psi \\in A \\} \\cup \\\\ ~~ \\{ \\phi \\mid \\phi \\wedge \\psi \\in A \\} \\cup \\\\ ~~ \\{ \\psi \\mid \\phi \\wedge \\psi \\in A \\} \\cup \\\\ ~~ \\{ \\phi \\mid \\psi \\in A, \\psi \\to \\phi \\in A \\}$\n\n$F$ is a montone function from the poset $\\langle \\mathcal P(X), \\subseteq \\rangle$ to itself. The reason that $F$ is monotone is that larger input sets give us more ways to apply the rules of our system, yielding larger outputs.\n\nIn addition to standard logical notions, deduction systems can be used to describe [type_system type systems], [program_logic program logics], and [operational_semantics operational semantics].\n\nAdditional material\n-------------\n\nIf you still haven't had enough monotonicity, might I recommend trying some of the [6pv exercises]?\n\n%comment:\nIncreasing functions\n----------------\n\nA monotone function between two [540 totally ordered sets] is called increasing. For example, the graph of a monotone function from the poset $\\langle \\mathbb R, \\le \\rangle$ to itself has an upward slope. Such functions can be searched efficiently using the [binary_search binary search algorithm]. \n%',
metaText: '',
isTextLoaded: 'true',
isSubscribedToDiscussion: 'false',
isSubscribedToUser: 'false',
isSubscribedAsMaintainer: 'false',
discussionSubscriberCount: '1',
maintainerCount: '1',
userSubscriberCount: '0',
lastVisit: '',
hasDraft: 'false',
votes: [],
voteSummary: [
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0',
'0'
],
muVoteSummary: '0',
voteScaling: '0',
currentUserVote: '-2',
voteCount: '0',
lockedVoteType: '',
maxEditEver: '0',
redLinkCount: '0',
lockedBy: '',
lockedUntil: '',
nextPageId: '',
prevPageId: '',
usedAsMastery: 'false',
proposalEditNum: '0',
permissions: {
edit: {
has: 'false',
reason: 'You don't have domain permission to edit this page'
},
proposeEdit: {
has: 'true',
reason: ''
},
delete: {
has: 'false',
reason: 'You don't have domain permission to delete this page'
},
comment: {
has: 'false',
reason: 'You can't comment in this domain because you are not a member'
},
proposeComment: {
has: 'true',
reason: ''
}
},
summaries: {},
creatorIds: [
'KevinClancy'
],
childIds: [],
parentIds: [
'poset_monotone_function'
],
commentIds: [],
questionIds: [],
tagIds: [],
relatedIds: [],
markIds: [],
explanations: [],
learnMore: [],
requirements: [],
subjects: [],
lenses: [],
lensParentId: 'poset_monotone_function',
pathPages: [],
learnMoreTaughtMap: {},
learnMoreCoveredMap: {},
learnMoreRequiredMap: {},
editHistory: {},
domainSubmissions: {},
answers: [],
answerCount: '0',
commentCount: '0',
newCommentCount: '0',
linkedMarkCount: '0',
changeLogs: [
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20578',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '14',
type: 'newEdit',
createdAt: '2016-12-03 23:54:32',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20563',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '13',
type: 'newEdit',
createdAt: '2016-12-03 02:47:41',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20558',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '0',
type: 'deleteTag',
createdAt: '2016-12-03 02:35:15',
auxPageId: 'work_in_progress_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20547',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '12',
type: 'newEdit',
createdAt: '2016-12-03 00:24:15',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20546',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '11',
type: 'newEdit',
createdAt: '2016-12-03 00:16:48',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20545',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '10',
type: 'newEdit',
createdAt: '2016-12-03 00:08:01',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20544',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '9',
type: 'newEdit',
createdAt: '2016-12-03 00:05:54',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20543',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '8',
type: 'newEdit',
createdAt: '2016-12-02 22:18:57',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20542',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '7',
type: 'newEdit',
createdAt: '2016-12-02 22:18:19',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '20541',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '6',
type: 'newEdit',
createdAt: '2016-12-02 22:04:18',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17523',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '4',
type: 'newEdit',
createdAt: '2016-07-26 15:04:07',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17522',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '3',
type: 'newEdit',
createdAt: '2016-07-26 15:02:58',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17521',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '2',
type: 'newEdit',
createdAt: '2016-07-26 15:00:35',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17511',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '0',
type: 'newParent',
createdAt: '2016-07-26 00:44:00',
auxPageId: 'poset_monotone_function',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17512',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '0',
type: 'newTag',
createdAt: '2016-07-26 00:44:00',
auxPageId: 'work_in_progress_meta_tag',
oldSettingsValue: '',
newSettingsValue: ''
},
{
likeableId: '0',
likeableType: 'changeLog',
myLikeValue: '0',
likeCount: '0',
dislikeCount: '0',
likeScore: '0',
individualLikes: [],
id: '17509',
pageId: 'order_monotone_examples',
userId: 'KevinClancy',
edit: '1',
type: 'newEdit',
createdAt: '2016-07-26 00:43:58',
auxPageId: '',
oldSettingsValue: '',
newSettingsValue: ''
}
],
feedSubmissions: [],
searchStrings: {},
hasChildren: 'false',
hasParents: 'true',
redAliases: {},
improvementTagIds: [],
nonMetaTagIds: [],
todos: [],
slowDownMap: 'null',
speedUpMap: 'null',
arcPageIds: 'null',
contentRequests: {}
}