# Calling recursion **URL:** \ **Category:** Learning\ **Created:** [February 18, 2021, 11:01am UTC](https://discuss.ocaml.org/t/calling-recursion/7306 "2021-02-18T11:01:06Z")\ **Posts on this page:** 8\ **Page:** 1
**Author:** ![jorge2705](https://avatars.discourse-cdn.com/v4/letter/j/898d66/32.png) [@jorge2705](https://discuss.ocaml.org/u/jorge2705)\ **Post date:** [February 18, 2021, 11:01am UTC](https://discuss.ocaml.org/t/calling-recursion/7306/1 "2021-02-18T11:01:06Z")
Hi, I am trying to implement a recursive call with the next code : ``` | Plus (x,y) -> begin match x, y with | x, Box y -> Box (Implies(x, y)) | x, Plus (a, b) -> Plus(x, Plus(a, b)) | x, y -> Implies(x, y) end ``` I am now testing the code with the next two cases : case 01 … +(p,[] z) it returns [](p =\> z) which is the correct translation for case 01. case 02 … +(p,+(q,[] z)) it should return [](p =\> (q =\> z)) , instead of that, it is going inside an infinity loop. I can see the problem is in the second line of the match, when I am calling Plus inside another Plus, but I understand the “exit” of the loop is given by the first line of the match. Could you give me any feedback to overcome this problem ? Thank you. Just to clarify, I am using the next translation for the operators Box [] Plus + Implies =\> ---
**Author:** ![shonfeder](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/shonfeder/32/424_2.png) [@shonfeder](https://discuss.ocaml.org/u/shonfeder)\ **Post date:** [February 18, 2021, 12:16pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/2 "2021-02-18T12:16:16Z")
Could you please show the full function you’re defining instead of just an excerpt from the case analysis? Also please format your examples as code, using the `` icon in the editor widget. There is no recursive call visible here at all (tho you are constructing a recursive data structure, but that cannot produce infinite loops on its own). ---
**Author:** ![jorge2705](https://avatars.discourse-cdn.com/v4/letter/j/898d66/32.png) [@jorge2705](https://discuss.ocaml.org/u/jorge2705)\ **Post date:** [February 18, 2021, 1:35pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/3 "2021-02-18T13:35:30Z")
Many thanks for your answer @shonfeder, in fact what I am trying to do is translate +(p,+(q,[] z)) to its equivalence sintaxt [](p =\> (q =\> z)) using the first and second lines of the match clause. ---
**Author:** ![shonfeder](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/shonfeder/32/424_2.png) [@shonfeder](https://discuss.ocaml.org/u/shonfeder)\ **Post date:** [February 18, 2021, 1:59pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/4 "2021-02-18T13:59:55Z")
Hi, @jorge2705. You still haven’t shown the entire function you are working with. Functions begin with ```auto let foo arg1 arg2 = ... ``` There is no way to introduce infinite loops in the code fragment you’ve shown, so we can’t help you identify the source of the problem yet 🙂 Perhaps it helps to point out that, given a type like ```auto 'a prop = | Plus of ('a, 'a) | Box of 'a | Implies of ('a, 'a) ``` An expression of the form `Plus (x, y)` is not usually referred to as "calling `Plus`". Rather, we say something like “you are constructing a value of type `'a prop` by applying the `Plus` constructor”. This is not "calling `Plus`" because `Plus` is not a function (in normal parlance). This is important here because merely applying a value constructor cannot produce an infinite loop. You may find it useful to review the section in the manual on records and variants: [Chapter 1  The core language](https://caml.inria.fr/pub/docs/manual-ocaml/coreexamples.html#s%3Atut-recvariants) ---
**Author:** ![shonfeder](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/shonfeder/32/424_2.png) [@shonfeder](https://discuss.ocaml.org/u/shonfeder)\ **Post date:** [February 18, 2021, 2:00pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/5 "2021-02-18T14:00:47Z")
Also, I’m afraid I missed the notification that this is your first post on the forum! Welcome to the OCaml Discuss! 👋 🙂 ---
**Author:** ![LdBeth](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ldbeth/32/2680_2.png) [@LdBeth](https://discuss.ocaml.org/u/LdBeth)\ **Post date:** [February 18, 2021, 2:35pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/6 "2021-02-18T14:35:52Z")
I think I can help rephrase the problem so it can help other people provide their solutions: giving the following rewriting rules ```nohighlight +(x, [] y) --> [] (=>(x, y)) ``` implement a (probably OCaml) program that rewrites an input form until no further rewrites can be applied and output it. an example trace of execution is ```auto +(p,+(q,[] z)) --> +(p, [](=>(q, z))) --> [](=>(p,=>(q,z))) ``` * * * Here’s my personal comments: I think a naive solution is having a recursive function does the pattern match and rewriting, and apply it until the result stays the same. And welcome to ocaml discuss! * * * probably more context on the problem can be helpful, I guess this is some kind of logical formulas, but I’m not a proper logician so I cannot identify what kind of logical system these symbols are from. ---
**Author:** ![jorge2705](https://avatars.discourse-cdn.com/v4/letter/j/898d66/32.png) [@jorge2705](https://discuss.ocaml.org/u/jorge2705)\ **Post date:** [February 18, 2021, 3:35pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/7 "2021-02-18T15:35:55Z")
Thank you @LdBeth for your feedback, and Yes , it is a rewriting problem, exactly as you explain in the example trace of execution (which reflects my testing case 02). And you are right again, this is a new logic , so I am trying to rewrite it in many steps until I finally arrive to its equivalence in propositional logic. So for example ` plus (a, plus(b, plus (c, box z)))` As you say, the translation should be `box(a => (b => (c => z)))` I will take into account your advice and try to use it to find a way to deal with this translation. Thank you for welcoming me to the group. ---
**Author:** ![jorge2705](https://avatars.discourse-cdn.com/v4/letter/j/898d66/32.png) [@jorge2705](https://discuss.ocaml.org/u/jorge2705)\ **Post date:** [February 18, 2021, 3:40pm UTC](https://discuss.ocaml.org/t/calling-recursion/7306/8 "2021-02-18T15:40:50Z")
Thank you @shonfeder for your feedback and welcoming to the group, I will take into account your suggestions and reference to try to find a solution to this rewriting problem.