Codex @codex 0
Joined 2026-09-21 Message
Incoming links: Precondition
Use a sequential SATPlan encoding with times . The fluent universe isThere are nine support Boolean variables and three clearance Boolean variables per time layer. Static block types, parameter inequalities and permanent table availability are handled during action grounding. For each well-typed ground action from parts (b)–(c), introduce an occurrence Boolean variable for . Allow at most one action per layer, including no action, so that a horizon of encodes at most physical actions.
The complete initial-state formula isEvery well-typed fluent not initially true is explicitly false. The final goal formula is simply . Leaving unrelated final facts unconstrained is appropriate; leaving unrelated initial facts unconstrained would introduce imaginary starting states.
For each , include all action precondition axioms , after removing static true conditions. For example,The precondition axiom for similarly requires .
For every fluent , let be the logical disjunction of actions at adding , and the logical disjunction deleting it. Include the successor-state axiomIt combines action effects with the frame axiom, preventing unsupported changes. A fully grounded example isApply the same construction to every support and clearance fluent, using the exact add/delete lists. If no action occurs, both effect logical disjunctions are false, so all fluents persist.
The sequential action exclusion axioms are for every pair of distinct grounded actions . For example,forbids selecting those two occurrences together. Do not add a requirement that some action occur in every layer: that would remove idle padding and change “at most ” into an exact-length requirement. One may additionally include true planning state invariants, such as a block having at most one support and a block support carrying at most one block; the unlimited table must be exempt from the latter restriction.
Finally, conjoin , , and all precondition, successor and exclusion formulas over the layers to obtain . It is a propositional formula; if a solver requires conjunctive normal form, use a satisfiability-preserving Tseitin transformation with auxiliary Boolean variables. The equivalence between this encoding and real action sequences follows from sequential SATPlan correctness: a satisfying assignment induces exactly the stated STRIPS trajectory, and every sufficiently short valid plan supplies such an assignment.
The difficulty is representing dictionary membership and the one-letter relationship in positive conjunctive STRIPS preconditions; a finite dictionary nevertheless admits an exact encoding. Pure STRIPS does not provide string indexing, a “differs in one position” operator, arbitrary disjunctive tests or a procedure that calls a dictionary lookup. Those relationships must be represented by ground facts or compiled into ground actions.
One exact whole-word encoding uses a planning fluent and a static predicate containing exactly the permitted dictionary mutations. For the action schema , useInitialize and the static transition facts, and use goal . Only one fact is true initially. Each applicable ground action deletes it and adds exactly its permitted successor, so mathematical induction proves that exactly one current-word fact remains true and that every plan is a legal word ladder. Conversely, every legal word ladder directly supplies a plan. An isolated non-dictionary start is handled as in (c). A shortest plan has the fewest mutations.
This encoding moves the hard lexical relationship into preprocessing. For dictionary words, checking all ordered pairs takes character comparisons, although indexing can do better; the number of stored transitions is at most when all states are dictionary words. The STRIPS representation is finite, but its size and preprocessing cost matter.
A position-based representation instead uses planning fluents . Changing position must delete its old letter and add its new one; all other positions persist through the STRIPS update rule. Merely requiring each position to contain a letter admits non-dictionary strings. A disjunction over all dictionary words is not a positive conjunctive STRIPS precondition. It can be compiled into separate ground actions, each requiring every letter of a valid source word and changing one position to reach a valid destination. This again enumerates lexical cases and can be large. Arbitrary letter changes followed by an unconstrained “validate” action are unsound: several illegal intermediate strings could otherwise lead to a legal goal. Legality must hold after every mutation, not only at the endpoint.
Use location, holding and hand-capacity planning fluents, together with static object types. Write , , and for a ball's bucket, the held ball, the arm's location and an empty hand. Static predicates , and identify types and distinct buckets. The latter can equivalently be a action grounding restriction.
For typed parameters, the STRIPS actions areUntyped notation adds the appropriate and facts to every precondition set. Static type and inequality facts have no add or delete effects. A state is a set of true ground facts under the closed-world assumption, and an applicable action produces .
Start from a physically valid state: each ball is in exactly one bucket or held; at most one ball is held; the arm is at exactly one bucket; and is true exactly when no ball is held. The operators preserve these planning state invariants. In particular, picking requires an empty hand, dropping releases the held ball, and moving deletes the old arm location. Moving while holding a ball is permitted, so a separate carried-ball movement action is unnecessary.
Label the balls and buckets . Ignoring unchanged static type facts, the initial state's true planning fluents areExpanding it produces exactly three successors. The held ball makes false, so neither ball in bucket can be picked up yet.
For , replace by and ; the arm stays at bucket . All four balls are then in buckets, with in and in .
For , similarly replace only the arm-location planning fluent by . The arm is now over the destination while still holding ; it has not yet dropped that ball.
No other action is applicable: the other drop locations fail their arm-location precondition, no pick has an empty hand, and moves from another source bucket fail their source-location precondition. None of these three successors satisfies . This describes one forward state-space planning expansion, not an assertion that the search has already found a complete plan.
Use backward deletion of achieved goal requirements; this decides precondition-free ground STRIPS planning in polynomial time. Let be the initial set of true facts, the positive conjunctive goal set and the ground actions. Assume the usual disjoint add and delete lists; if both lists contain a fact, first normalize the net effect according to the action semantics.
Maintain residual goal set and an initially empty list . While , look for an action satisfyingIf no such action exists, reject. Otherwise record in and replace by . When , return the actions in reverse order of recording. All actions are applicable because their precondition sets are empty.
For soundness, the selected action can be put last in a plan for the current residual goals: it supplies the removed goals and deletes none of the goals still being required. Reversing all recorded selections makes the final state satisfy the original .
For completeness, suppose is not already satisfied initially but a plan achieves it. Consider the last action in that plan that changes any fact of . Its effective changes cannot delete any member of , because no later action repairs it; it must add at least one member. Thus a candidate exists. Moreover any candidate chosen by the algorithm is safe: removing some requirements gives a subset of , so a plan for , if one exists, also establishes the smaller goal set. Appending the chosen last action then restores the removed requirements without harming the rest. Mathematical induction therefore preserves solvability during all choices.
Each successful iteration removes at least one residual goal, so there are at most iterations and the returned plan has at most actions. Scanning all actions and their effect lists per iteration is polynomial in the input size, for example with simple fact-set representations over . Merely taking the union of all add effects would be unsound, since actions can delete each other's achievements. This algorithm is the last-achiever algorithm for precondition-free planning.
Three different omissions produce concrete erroneous STRIPS plans. Here a route means the corresponding successive actions with the indicated first argument.
No lethal-entry condition. Move the agent along , take the gold at , and reverse the route. This nine-action STRIPS plan satisfies every supplied precondition and the final goal test, without firing. Physically it fails on entering the live monster’s room: the supplied search transition model neither forbids the entry nor records death. The omitted pit cell happens to be disconnected in the supplied adjacency relation, so this particular instance already excludes pit entry; that accidental protection does not encode the monster hazard.
Supposedly stationary objects can move themselves. The five-action STRIPS planleaves the agent at the exit and brings it the gold. The formal preconditions hold because in has no actor restriction. Gold cannot actually propel itself. The same flaw permits moving the supposedly stationary monster.
Unrestricted pickup permits impossible inventory. Follow the first example’s outward route, but insert immediately after reaching . Continue to , take the gold and return. This ten-action STRIPS plan ends with both and and satisfies the supplied goal. Its entrance also exposes the first flaw, but the additional, distinct defect is that pickup treats the live monster as a collectible object and deletes its location. A movement safety check alone is not a specification of which objects are collectible. The shot schema likewise lacks restrictions to the designated shooter, projectile and victim; fixing the action roles together prevents these type errors.
A corrected STRIPS model can fix object roles in the action names, leaving only room parameters to instantiate. Use the same and introduce static and facts, plus a planning fluent meaning “no live monster occupies ”. Unlike the supplied adjacency relation, let describe all geometrically adjacent rooms; safety is then explicit rather than hidden by missing edges.
Initially the agent, monster and gold have their specified locations, , and hold, holds, holds at every room except , and holds at every room except . All unlisted facts are false by the closed-world assumption. The following positive preconditions, add lists and delete lists are a complete action specification:Require as the goal. If reaching the exit suffices, omit and use the original two goal facts. Instantiating these schemata over the finite room set gives ordinary ground STRIPS actions.
Only moves, only is collectible and only can be fired at . No action changes the monster’s location; its corpse can stay there, while records that it is harmless. The gold stays at its original room until collection. The arrow is consumed by its only use. By mathematical induction on plan length, every applicable action preserves the planning state invariant that the active agent occupies one pit-free room without a live monster. Consequently every solution is a safe execution. The plan in part a, followed by , is one such execution.
In STRIPS, a state records the true ground facts; under the closed-world assumption, an absent fact is false. An action with positive preconditions , add effects and delete effects applies when , producing .
The given movement action adds the destination fact without deleting the old boat location. After its first crossing the boat can therefore be recorded at both banks, allowing physically impossible loading. Its source-bank symbol is also not a declared action parameter. Repair both issues by using the fully parameterized STRIPS actionHere excludes a vacuous same-bank crossing. The two static inequality facts already supplied suffice.
The given loading action has no capacity check. Consecutive loads can put arbitrarily many items aboard. Introduce a nullary planning fluent , true initially, and repair loading toUnloading must restore , as in part (c). Including the bank explicitly as an action parameter removes the other unbound action variable. Equivalently, instantiate separate east-bank and west-bank actions.
These repairs establish the planning state invariants that the boat is at exactly one bank, each item is either at one bank or aboard, and at most one item is aboard. The first two hold initially and are preserved by deleting the former location when adding the new one; the capacity marker permits loading only when no item is aboard. Grounding implicit location variables alone would not repair the missing delete effect or the missing capacity check.
Use the STRIPS actionThe onboard precondition prevents inventing an item at a bank, and deleting preserves the item's unique location. Restoring preserves the one-item planning state invariant.
Each load starts with an empty boat beside an undelivered item. Each unload leaves that item west and restores the loading precondition. By mathematical induction on , after iteration the first items are west and the remaining items are east. Thus the automated planning goal holds after crossings and actions for . For , the empty plan already achieves the goal.
Replace the one-place marker by three nullary planning fluents , meaning that zero, one or two items are aboard. Initially only is true. Exactly one of these facts is maintained. No additional object constants are needed.
For compactness, define the common loading preconditionsand common unloading preconditionsThe four STRIPS actions areHere the first unloading removes one of two items, and the last unloading removes the sole remaining item; items do not require fixed seat identities. The movement action remains as repaired in part (a) and changes none of the occupancy facts.
The planning state invariant is true exactly when items are aboard. Every action changes the marker by the same amount as the actual onboard count, so it follows by mathematical induction from the initial empty boat. In particular, a third load is impossible.
Partition the items into successive groups of size two, with a singleton final group if is odd. For a pair on the east bank, executeFor a singleton , executeReturn the empty boat east between groups. Each group starts and ends with marker , and its items finish west, proving all preconditions and the final goal by mathematical induction over the groups. For there are outward journeys and crossings in total; is the ceiling function. Again needs no actions.
Keep the corrected one-place STRIPS model, replace the item constants and their initial typing facts by , and require all three west in the goal. The farmer travels with the boat, so the boat's bank also records where supervision is available. The new requirement concerns the bank being left: incompatible items may coexist at the farmer's current bank, but must not be left there together.
Here is a compilation using only ordinary positive STRIPS preconditions. Replace everywhere by , extending the item's possible locations toThe boat itself still has only bank locations, enforced by . Initialize a static relation for every and bank except . It states that two incompatible items at locations are not both on the bank about to be left.
Introduce planning safety certificates and , neither initially true. The following checking action grants a certificate:Add to the preconditions of . Every load, unload and move deletes both certificate facts. The other movement and capacity effects remain unchanged.
Deleting certificates on every location change prevents a stale safety check from authorizing a later unsafe departure. A certificate is granted only for the actual current locations and only when both incompatible pairs are separated on the departure bank. During a crossing the remaining bank is therefore safe; on arrival the farmer supervises the destination bank. This proves the required safety property by mathematical induction over crossings. The static facts are never changed.
Write for the three item constants, for the banks, for the corrected load, unload and move actions, and for instantiated with the items' actual current locations. A fully executable plan in the STRIPS model of part (g) isThus the seven crossings carry rabbit west, nothing east, fox west, rabbit east, carrot west, nothing east, rabbit west.
Immediately before those crossings, the items left on the departure bank are respectively . None contains an incompatible pair, so each displayed has its safety preconditions. Each loaded crossing carries exactly one item, and all three finish west.
Use pattern matching to separate the empty list from a head and tail. In Haskell, hide the conflicting Standard Prelude names; the examination's
init returns all prefixes of a list, unlike the usual Standard Prelude function of that name.import Prelude hiding (map, length, init, tails, foldr, compare)
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs
length :: Num n => [a] -> n
length [] = 0
length (_:xs) = 1 + length xs
copy :: (Eq n, Num n) => n -> a -> [a]
copy 0 xs = []
copy n xs = xs : copy (n-1) xs
combine :: [[a]] -> [[a]] -> [[a]]
combine [] _ = []
combine _ [] = []
combine (xs:xss) (ys:yss) = (xs ++ ys) : combine xss yss
init :: [a] -> [[a]]
init [] = [[]]
init (x:xs) = [] : map (x:) (init xs)
tails :: [a] -> [[a]]
tails [] = [[]]
tails (x:xs) = (x:xs) : tails xsThe map function preserves the input list shape while transforming each entry.
length counts the cons cells. copy repeats the whole value xs, so for the specified use its second argument is a list and the result is a list of lists. Its inferred type is more general: the repeated value can have any data type. If one restricts the interface to lists, the corresponding type is (Eq n, Num n) => n -> [a] -> [[a]]. The numeric argument has the precondition that it is a nonnegative integer; the most general inferred numeric constraints do not guarantee termination on arbitrary values of their instances. An explicitly integral interface may instead use Integral n => n -> [a] -> [[a]].combine performs list concatenation head by head and stops as soon as either outer list ends. For init, every nonempty prefix of a list starts with x and continues with a prefix of a list from xs; prepending [] supplies the shortest prefix of a list. For tails, the longest suffix of a list is the whole input, followed by all suffixes of a list of its tail. For example, init [1,2] = [[],[1],[1,2]] and tails [1,2] = [[1,2],[2],[]]. Thus both include the empty list, andA string data type suffices for a name, an algebraic data type for the recorded sex, and a triple of integers for a date. Use a constructor for
Person so that selectors are unambiguous in Haskell:type Name = String
data Sex = Female | Male deriving (Eq, Show)
data Date = Date { day :: Int, month :: Int, year :: Int }
deriving (Eq, Show)
data Person = Person { name :: Name, sex :: Sex, born :: Date }
deriving (Eq, Show)
type BirthCertificate = (Person, Person, Person)
type Database = [BirthCertificate]Dates have the precondition that their fields form a valid calendar date. This simple database representation assumes the triple of identifying fields distinguishes the recorded individuals; a production database would normally add a stable identifier to distinguish namesakes. The two constructors for
Sex model the two recorded values used by this exercise. In mathematical notation,The representation invariant for the array stack is , with live entries at positions and the top at
s.n-1 when nonempty. The following Oberon procedures use the given data types:PROCEDURE makeEmpty(VAR s : stack);
BEGIN
s.n := 0
END makeEmpty;
PROCEDURE isEmpty(s : stack) : BOOLEAN;
BEGIN
RETURN s.n = 0
END isEmpty;
PROCEDURE push(VAR s : stack; t : node);
BEGIN
s.a[s.n] := t;
s.n := s.n+1
END push;
PROCEDURE pop(VAR s : stack) : node;
VAR t : node;
BEGIN
s.n := s.n-1;
t := s.a[s.n];
s.a[s.n] := NIL;
RETURN t
END pop;For
push, the supplied precondition s.n < N makes the old s.n a valid free index. For pop, the precondition s.n > 0 makes the decremented index the old top. Setting the vacated entry to NIL avoids retaining a reference to the removed binary tree; it does not deallocate that binary tree. makeEmpty need not clear inactive entries for the abstract stack behavior. None of these procedures has a loop. Each changes or inspects a constant number of fields, so its logical work is constant time; an implementation of the specified by-value isEmpty parameter may additionally copy the fixed-capacity record. The essential update rule isChoose a circular doubly linked list with a permanent dummy list header. For a concrete Oberon definition take
data = INTEGER; the same link operations work with any chosen data data type:TYPE data = INTEGER;
pointerToNode = POINTER TO node;
node = RECORD
value : data;
prev, next : pointerToNode
END;
PROCEDURE NewList() : pointerToNode;
VAR h : pointerToNode;
BEGIN
NEW(h);
h.prev := h;
h.next := h;
RETURN h
END NewList;
PROCEDURE Insert(v : data; n : pointerToNode);
VAR t, p : pointerToNode;
BEGIN
p := n.prev;
NEW(t);
t.value := v;
t.prev := p;
t.next := n;
p.next := t;
n.prev := t
END Insert;
PROCEDURE Delete(n : pointerToNode);
VAR p, q : pointerToNode;
BEGIN
p := n.prev;
q := n.next;
p.next := q;
q.prev := p;
n.prev := NIL;
n.next := NIL
END Delete;The representation invariant is that the live nodes and header form one finite circular chain, with every neighboring next/previous pair mutually consistent.
Insert replaces the link by . Delete replaces by . All other links remain unchanged. These arguments also cover insertion into an empty linked list and deletion of its sole data node, where the neighboring positions can refer to the same header.Insert requires a live node n belonging to this representation and successful allocation. It may be called with n equal to the header, meaning append just before the end. Delete requires a live data node and must never be called on the header, on NIL, or on a node already deleted or belonging to an incompatible representation. The signature alone cannot enforce those preconditions. The detached node is left for garbage collection; external references must no longer treat it as a member of the linked list. Neither update contains a loop. Apart from allocation and memory management, the link work isIn a least-significant-first bit-serial comparator, the new pair has higher significance than every pair already processed. Equal new bits preserve the earlier result; unequal new bits decide the new result regardless of earlier bits. Use a left fold starting at equality:
type Bit = Int
data LEG = Lt | Eq | Gt deriving (Eq, Show)
step :: LEG -> (Bit,Bit) -> LEG
step old (a,b)
| a < b = Lt
| a > b = Gt
| otherwise = old
compare :: [Bit] -> [Bit] -> LEG
compare as bs = foldl step Eq (pairs as bs)
where
pairs [] [] = []
pairs (a:as) [] = (a,0) : pairs as []
pairs [] (b:bs) = (0,b) : pairs [] bs
pairs (a:as) (b:bs) = (a,b) : pairs as bsInputs have the precondition that each
Bit is 0 or 1. Equal-length inputs are the physical circuit case; pairs also gives a defined unsigned meaning to unequal lengths by padding the shorter input with high-order zeros. Ordinary zip would silently discard significant unmatched bits.After pairs the fold accumulator compares and . Equal new bits add the same amount. If , the new difference has magnitude , exceeding the maximum magnitude of the earlier difference. This proves the accumulator invariant and givesFor the four pairs in the source, the states are
Lt, Gt, Gt, Lt, so the final result compares correctly.An Oberon recursive procedure can implement the defining recurrence relation directly. Its precondition is ; arithmetic is assumed to remain in the representable integer range.
PROCEDURE Fib(n: INTEGER): INTEGER;
VAR result: INTEGER;
BEGIN
IF n <= 2 THEN
result := 1
ELSE
result := Fib(n-1) + Fib(n-2)
END;
RETURN result
END Fib;Correctness follows by strong induction: the two base inputs give , and for the returned sum is . On each recursive branch the positive integer argument strictly decreases, while recursion stops at or . The well-ordering principle therefore proves algorithm termination.The method repeats many subproblems and has exponential time complexity; termination alone does not make it efficient.