Hi, all. Though I'm not a native english speaker, but I think that the keyword 'do' looks so imperative. It's a good idea to use another keyword to make it look more declarative, for example, like 'for ... that P(....)' . <div class="gmail_quote">在 2014-1-18 下午12:00，"Mark Brown" <<a href="mailto:mark@mercurylang.org">mark@mercurylang.org</a>>写道： <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Hi everyone, Here is a concrete proposal for "inductive goals" in Mercury. I'm going to avoid calling these "loops", since logic programmers understandably take a dim view of these (hint: if it terminates, it's not really a loop). The goals are called inductive because they are logically equivalent to the conjunction of a sequence of goals, with this sequence being inductively defined. They could also be called "for" goals, since that is the keyword they begin with. This follows on from the "Adding Loops to Mercury" thread earlier this month, but I've started a new thread for this specific proposal. This is to put the design on the record. I'm not planning to implement it myself at this time. Would this meet people's requirements? Cheers, Mark. Inductive Goals ---------------------- 1. Background The declarative semantics is essentially that of the "more complicated" version of sequence quantifiers that Fergus Henderson writes about [1], which are based on Peter Schachte's Sequence Quantification [2]. The operational semantics are derived from Sebastian Brand's generic inline iteration proposal [3], which in turn is derived from Joachim Schimpf's Logical Loops [4]. The main challenge for Mercury is to perform the Logical Loops translation in such a way that precise determinisms are preserved. This proposal achieves that by using available mode information to direct the translation. [1] <a href="http://lists.mercurylang.org/pipermail/developers/2000-December/010812.html" target="_blank">http://lists.mercurylang.org/pipermail/developers/2000-December/010812.html</a> [2] <a href="http://lists.mercurylang.org/pipermail/developers/2014-January/015962.html" target="_blank">http://lists.mercurylang.org/pipermail/developers/2014-January/015962.html</a> [3] <a href="http://lists.mercurylang.org/pipermail/developers/2005-December/013919.html" target="_blank">http://lists.mercurylang.org/pipermail/developers/2005-December/013919.html</a> [4] <a href="http://www.eclipseclp.org/reports/index.html" target="_blank">http://www.eclipseclp.org/reports/index.html</a> 2. Sequences We start by defining two kinds of sequence: which I will call map sequences and fold sequences. For a given sequence of values, the map sequence is just those values in the same order, while the fold sequence is the sequence of consecutive pairs of values. So for the values 1, 2, 3, 4, 5, we have: elements of map sequence: 1, 2, 3, 4, 5 elements of fold sequence: (1, 2), (2, 3), (3, 4), (4, 5) The actual values involved will be defined inductively by the goal body. Two or more sequences "correspond" if they are all of the same length. Note that this implies that fold sequences contain one more value than corresponding map sequences, since they include both the initial and final value. 3. Syntax Inductive goals are written like this: for $sequence, ... mismatch $mismatch do $body The intuitive meaning of this is to iterate over all sequences in lockstep, executing $body for each set of corresponding elements, and executing $mismatch if the sequences don't correspond. The mismatch goal is optional, and defaults to throwing a software error. If given, the mismatch goal is not allowed to succeed (i.e., it must have determinism failure or erroneous). Sequences are written in one of the following forms: $X maps $Xs [$Current, $Next] folds [$First, $Last] [$A0, $A] The first says that $X is an element in the map sequence defined by $Xs. The second says that ($Current, $Next) is an element in the fold sequence whose first value is $First and whose last value is $Last. The third is just shorthand for '[$A0, $A] folds [$A0, $A]', and can be used if $A0 and $A are Mercury variables (the other forms can be used with arbitrary Mercury expressions). Mercury variables on the left hand side of 'maps' or 'folds' are quantified in the body. Those on the right hand side are free (i.e., non-local to the inductive goal). For the shorthand form, $A0 and $A stand for two pairs of variables with the same names, one pair of which is quantified in the body while the other is free. 4. Examples Here's how to implement a few of the existing list.m library predicates. all_true(P, Xs) :- for X maps Xs do P(X). map(P, Xs, Ys) :- for X maps Xs, Y maps Ys do P(X, Y). length(Xs, N) :- for _ maps Xs, [I, I + 1] folds [0, N] do true. map_corresponding3_foldl(P, As, Bs, Cs, Ds, !S) :- for A maps As, B maps Bs, C maps Cs, D maps Ds, [!S] mismatch throw("list.map_corresponding3_foldl: length mismatch") do P(A, B, C, D, !S). The code for map3_foldl is the same as for map_corresponding3_foldl, except that the mismatch clause isn't needed. These predicates are effectively different modes of the same inductive goal. Sequences that can fail can be useful: take(N, List, Start) :- for [I, I + 1] folds [0, N], [[X | Xs0], Xs0] folds [List, _], % can fail X maps Start do true. The do goal can refer to non-local variables, although it is not allowed to bind them. This example refers to the non-local Stream variable to print the elements in a list: write_elements(Stream, Xs, !IO) :- for X maps Xs, [!IO] do write(Stream, X, !IO), nl(Stream, !IO). Filtering is not done by the construct itself, but is easily done in the body: filter_map_corresponding(F, As, Bs) = Cs :- for A maps As, B maps Bs, [Cs1, Cs0] folds [Cs, []] mismatch throw("filter_map_corresponding/2: length mismatch") do ( if C = F(A, B) then Cs1 = [C | Cs0] else Cs1 = Cs0 ). Here's an example that calls P on all the unordered pairs of elements of list Xs, with accumulator !A: for [[X | Tail], Tail] folds [Xs, []], [!A] do for Y maps Tail, [!A] do P(X, Y, !A). Here's an example of iterating over a sequence defined by the functions empty/0, next/1 and value/1: for [S, next(S)] folds [Start, empty], [!IO] do write(value(S), !IO). Here's a similar example using function empty/0 and predicate next/3: for [!S] folds [Start, empty], [!IO] do next(I, !S), write(I, !IO). One thing that inductive goals can't do is use a predicate to decide if the sequence is empty. The test for whether the sequence is empty is done by unifying the sequence with a specific value. So an integer sequence can end with a test like I = N, but not one like I > N. The same effect, however, can be obtained by adding an extra sequence of booleans that say whether the induction should continue: % Counts while $Test succeeds. for [I, I + 1] folds [0, _], [!Continue] folds [yes, no] do ( if $Test then $Body else !:Continue = no ). As a final example, inductive goals can also be used to generate sequences of all lengths. This goal generates all lists of 0s and 1s: for X maps Xs do ( X = 0 ; X = 1 ). 5. Semantics The meaning of the inductive goal is given by universally quantifying over all sequence positions. So for example the goal: for $X maps $Xs, [$Current, $Next] folds [$First, $Last], [$A0, $A], ... do $Body means the following: all [I] ( $X is the I'th element of $Xs /\ $Current is the I'th value of the first fold sequence /\ $Next is the (I+1)'th value of the first fold sequence /\ $A0 is the I'th value of the second fold sequence /\ $A is the (I + 1)'th value of the second fold sequence /\ ... => $Body ) 6. Types and Modes Types are determined by the type signatures of the sequence expressions, which are as follows: all [T] (T maps list(T)) all [T] ([T, T] folds [T, T]) These ensure each sequence is typed consistently, but allow different sequences to have unrelated types. Like types, modes are determined by the mode signatures of the sequence expressions. For each form of sequence there is a selection of modes to choose from. This choice is made for each sequence independently. The modes are as follows: % Input modes: in(I) maps in(list(I)) [in(I), out(I)] folds [in(I), in(I)] % Output modes: out(I) maps out(list(I)) [in(I), out(I)] folds [in(I), out(I)] [mdi, muo] folds [mdi, muo] [di, uo] folds [di, uo] [out(I), in(I)] folds [out(I), in(I)] Sequences with input modes determine the number of iterations that are generated. Sequences with output modes work with any number of iterations. In order to schedule an inductive goal, the mode analyser needs to schedule all sequences at the same time. This involves checking that, for each fold sequence, at least one of the terms on the right hand side is instantiated. Scheduling should probably be delayed until as many sequences are in the input mode as possible, which will ensure the strongest determinism result. Note that all inst variables will be bound when the goal is scheduled, so inst variables won't need to appear in generated code. 7. Determinism In Mercury, the determinism of a goal or expression is specified by the answers to three questions: - Can the goal or expression fail? - Can the goal produce multiple solutions? (Expressions aren't allowed to do this.) - Does the goal or expression have to be evaluated in a committed choice context? For any of these questions, if the answer is yes for the body goal or the head expressions on the right hand side of the sequence operators, then it is yes for the inductive goal as a whole. This is also true for the expressions on the left hand side of the sequence operators, with one exception. The exception is that, in the input mode for 'folds', the first argument on the left hand side is never tested against the value of the second argument on the right hand side; had it taken that value, the inductive goal would already have terminated. So this expression does not itself need to be proven never to fail. If it does actually ever fail on some other value, the inductive goal either fails or the mismatch goal is executed (behaviour in this respect is undefined - in the translation below it fails if all sequences are output, but throws the mismatch exception in all other modes). Aside from the previous paragraph, the only other way an inductive goal can fail is if the mismatch goal fails, which can only occur if it has a failure determinism. The only other way an inductive goal can produce multiple solutions is if all sequences are in the output mode. There are no other circumstances in which an inductive goal must be evaluated in a committed choice context. 8. Translation Inductive goals are translated at compile time into a call to a compiler generated predicate. The predicate is passed the following arguments: - One argument for each non-local variable occurring in the body or in the mismatch goal. - One argument for each map sequence. - Two arguments for each fold sequence. In the first case, the arguments are the non-local variable themselves. In the other two cases, the arguments are those expressions appearing on the right hand side of the relevant sequence. For example, Separator is non-local in the following goal: for X maps Xs, [!IO] do write(X, !IO), write_string(Separator, !IO) This is translated into the call: $predname(Separator, Xs, !IO) where $predname is the name of the generated predicate. In the signature of the generated predicate, the types of the parameters are determined directly from the types of the arguments listed above. For each of the non-local arguments the mode is 'in(I)', where I is the inst of the non-local at the time the call is scheduled. For the other arguments, the mode is determined by the selected mode of the sequence in question. The determinism can be inferred according to the rules given earlier. For the example above, $predname would be given the following signature: :- pred $predname(string::in, list(T)::in, io::di, io::uo) is det. The head of the generated clause uses the same names for the non-local head variables as are used in the original goal. For map sequences, the head variables are named _M1, _M2, etc, and for fold sequences they are named _Fa1, _Fb1, _Fa2, _Fb2, etc. For each sequence we define two goals, the end goal and the step goal. The end goal defines the end of the sequence, while the step goal defines each step along the way. For i'th map sequence '$X maps $Xs', the goals are: end goal: _Mi = [] step goal: _Mi = [$X | _Mri] where _Mri is a fresh variable. For the i'th fold sequence '[$Current, $Next] folds [$First, $Last]', the goals are: end goal: _Fai = _Fbi step goal: _Fai = $Current The generated clause makes one recursive call to itself. The non-locals are passed as is. For the i'th map sequence, the recursive argument is _Mri. For the i'th fold sequence, the two arguments are $Next and _Fbi. The general form of the generated clause body depends on which of the sequences are used in an input mode, and which are output. If there is at least one input sequence, the body has this general form: ( if conjunction of input end goals then conjunction of output end goals else if conjunction of input step goals then conjunction of output step goals, $Body, recursive call else $Mismatch ). If all of the sequences are output, the body has this general form: ( conjunction of end goals ; conjunction of step goals, $Body, recursive call ). The example from above is repeated here: for X maps Xs, [!IO] do write(X, !IO), write_string(Separator, !IO) For this inductive goal, which is called with the first sequence in the input mode, we generate the following clause (with state variable !IO expanded out to _IO_i): $predname(Separator, _M1, _Fa1, _Fb1) :- ( if _M1 = [] then _Fa1 = _Fb1 else if _M1 = [X | _Mr1] then _Fa1 = _IO_0, write(X, _IO_0, _IO_1), write_string(Separator, _IO_1, _IO_2), $predname(Separator, _Mr1, _IO_2, _Fb1) else error("length mismatch in inductive goal") ). 9. Example translations Here are the translations for a few of the examples from earlier. The declarations include the determinism that ought to be inferred for the introduced predicates. Here is length/2 again: length(Xs, N) :- for _ maps Xs, [I, I + 1] folds [0, N] do true. In the (in, out) mode, this translates to: length(Xs, N) :- aux_1(Xs, 0, N). :- pred aux_1(list(T)::in, int::in, int::out) is det. aux_1(_M1, _Fa1, _Fb1) :- ( if _M1 = [] then _Fa1 = _Fb1 else if _M1 = [_ | _Mr1] then _Fa1 = I, true, aux_1(_Mr1, I + 1, _Fb1) else error("length mismatch in inductive goal") ). Here is map_corresponding3_foldl/7 again: map_corresponding3_foldl(P, As, Bs, Cs, Ds, !S) :- for A maps As, B maps Bs, C maps Cs, D maps Ds, [!S] mismatch throw("list.map_corresponding3_foldl: length mismatch") do P(A, B, C, D, !S). The mode of the sequences is (in, in, in, out, out), so we generate this: :- pred aux_2( pred(A, B, C, D, S, S)::in(pred(in, in, in, out, in, out) is det), list(A)::in, list(B)::in, list(C)::in, list(D)::out, S::in, S::out) is det. aux_2(P, _M1, _M2, _M3, _M4, _Fa1, _Fb1) :- ( if _M1 = [], _M2 = [], _M3 = [] then _M4 = [], _Fa1 = _Fb1 else if _M1 = [A | _Mr1], _M2 = [B | _Mr2], _M3 = [C | _Mr3] then _M4 = [D | _Mr4], _Fa1 = _S_0, P(A, B, C, D, _S_0, _S_1), aux_2(P, _Mr1, _Mr2, _Mr3, _Mr4, _S_1, _Fb1) else throw("list.map_corresponding3_foldl: length mismatch") ). If the mode of the sequences was (in, out, out, out, in, out), and without a mismatch clause, then we would instead generate code like map3_foldl: :- pred aux_3( pred(A, B, C, D, S, S)::in(pred(in, out, out, out, in, out) is det), list(A)::in, list(B)::out, list(C)::out, list(D)::out, S::in, S::out) is det. aux_3(P, _M1, _M2, _M3, _M4, _Fa1, _Fb1) :- ( if _M1 = [] then _M2 = [], _M3 = [], _M4 = [], _Fa1 = _Fb1 else if _M1 = [A | _Mr1], then _M2 = [B | _Mr2], _M3 = [C | _Mr3], _M4 = [D | _Mr4], _Fa1 = _S_0, P(A, B, C, D, _S_0, _S_1), aux_3(P, _Mr1, _Mr2, _Mr3, _Mr4, _S_1, _Fb1) else error("length mismatch in inductive goal") ). Here is take/3 again: take(N, List, Start) :- for [I, I + 1] folds [0, N], [[X | Xs0], Xs0] folds [List, _], % can fail X maps Start do true. We would generate: :- pred aux_4(list(T)::out, int::in, int::in, list(T)::in, list(T)::out) is semidet. aux_4(_M1, _Fa1, _Fb1, _Fa2, _Fb2) :- ( if _Fa1 = _Fb1 then _M1 = [], _Fa2 = _Fb2 else if _Fa1 = I then _M1 = [X | _Mr1], _Fa2 = [X | Xs0], true, aux_4(_Mr1, I + 1, _Fb1, Xs0, _Fb2) else error("length mismatch in inductive goal") ). Note that the unification of _Fa2 and [X | Xs0] can fail, making the whole predicate semidet. This occurs when there are not enough elements in List for the given value of N. Here's the goal to generate all lists of zeroes and ones: for X maps Xs do ( X = 0 ; X = 1 ) We would generate: :- pred aux_5(list(int)::out) is multi. aux_5(_M1) :- ( _M1 = [] ; _M1 = [X | _Mr1], ( X = 0 ; X = 1 ), aux_5(_Mr1) ). _______________________________________________ developers mailing list <a href="mailto:developers@lists.mercurylang.org">developers@lists.mercurylang.org</a> <a href="http://lists.mercurylang.org/listinfo/developers" target="_blank">http://lists.mercurylang.org/listinfo/developers</a> </blockquote></div>