Hi, thanks for the cool tool!
I am currently experimenting with using stitch to augment a theorem prover for equational logic. As such, I'm only dealing with first order terms. Do you think it would be easy to add some kind of first-order flag that would force stitch to avoid producing higher order abstractions?
To illustrate what I mean by the higher-order abstractions I would like to avoid, suppose we have the following programs:
programs = [
'(lam (lam (op (op b $0) (op b $1))))',
'(lam (lam (op (op c $0) (op c $1))))'
]
Then running compress(programs, iterations=1, max_arity=2) gives the following abstraction:
fn_0(#0) := (lam (lam (op (#0 $0) (#0 $1))))
which is higher-order since it takes in a function as an argument.
This issue of restricting to first-order terms seems like it would also be relevant to another issue, since I would also want to avoid assuming we are dealing with curried functions. But this seems easier to deal by just post-processing the abstractions to produce first-order ones.
Do you have any ideas on this? Perhaps you could point me to the relevant source code and I could work on making a PR?
All the best
Hi, thanks for the cool tool!
I am currently experimenting with using stitch to augment a theorem prover for equational logic. As such, I'm only dealing with first order terms. Do you think it would be easy to add some kind of first-order flag that would force stitch to avoid producing higher order abstractions?
To illustrate what I mean by the higher-order abstractions I would like to avoid, suppose we have the following programs:
Then running
compress(programs, iterations=1, max_arity=2)gives the following abstraction:which is higher-order since it takes in a function as an argument.
This issue of restricting to first-order terms seems like it would also be relevant to another issue, since I would also want to avoid assuming we are dealing with curried functions. But this seems easier to deal by just post-processing the abstractions to produce first-order ones.
Do you have any ideas on this? Perhaps you could point me to the relevant source code and I could work on making a PR?
All the best