0

This question is based on my question https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re There are two functions and two terms in that question:

Functions:

is: (e->t)->(e->t)
IS: e->(e->t)->t

Terms:

(is(boss))(John): t
IS(John, boss): t

My question is this: how to rewrite terms involving is with terms that have only IS? Does Coq (or third party tools) has such rewriting facilities? Does Coq have facilities to check the equality of rewrittern terms?

Maybe such rewriting can be done outside the Coq world, maybe there are other purely lambda calculus tools with syntactic manipulation only?

TomR
  • 2,696
  • 6
  • 34
  • 87
  • 1
    Do you want to perform this rewriting in the middle of a proof? Or do you want to edit existing Coq definitions that mention `is` so that they only mention `IS`? – Arthur Azevedo De Amorim Aug 24 '18 at 14:06
  • 1
    Note that the form `is boss John`, which is syntactically equivalent to `(is(boss))(John)`, is less verbose than `IS(John, boss)`. Chained function application is usually preferred in Coq. – Arthur Azevedo De Amorim Aug 24 '18 at 14:08
  • I would prefer two separate theories - one with “is“ and another - transformed one - with “IS“. I will generate the first theory from GrammaticalFramework and then I would like to transform it into the second one. – TomR Aug 24 '18 at 14:13
  • The second “IS“ form can be more easily converted to is-boss predicate, that is why I am striving to arrive at it. Predicate form can be used for reasoning with object logics that are mechanized in Coq, e.g., with linear logics. – TomR Aug 24 '18 at 14:18
  • If `boss` has type `e -> t`, `e` means "entity" and `t` stands for the Booleans, couldn't you just use `boss John`? – Arthur Azevedo De Amorim Aug 24 '18 at 14:29

1 Answers1

1

There is no tool that performs the kind of textual transformation of Coq code you are describing directly. Without knowing much about GrammaticalFramework, I imagine that your best bet would be to write a Sed script that looks for occurrences of is applied to arguments and replaced those occurrences by equivalent expressions with IS.

The second “IS“ form can be more easily converted to is-boss predicate, that is why I am striving to arrive at it.

I think that if you used a Sed script you could just as easily go to the IS_BOSS form directly, without using IS.

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39