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 =>
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).
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.
You still haven’t shown the entire function you are working with. Functions begin with
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
'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
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.
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.
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.
