The Coq mailing list

[Alex Meyer <alex153 AT outlook.lv>]

I am reading https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v and

http://subsell.logic.at/bio-CTC/ and I am trying to declare in this encoding of linear logic

- constant "John"

- function "thinks(John)"

(I am trying to apply this framwork for the formal semantics of natural language - e.g. in style of https://www.stergioschatzikyriakidis.com/research-outputs.html etc.), that is why I am having such function).

I have arrived at the following expressions:

cte(John)

Cte(John) := fun _ => cte(John)

but I don't know how to arrive at the final _expression_ of type ClosedT:

cl_cte: forall C, closedT(fun _ => cte(C)) - where can I put John here?

The same thing is with function:

fc1(1, cte(John))

FC1(1, Cte(John))

FC1(1, fun _ => cte(John)) =

= fun __ => fc1 (1, fun _ => cte(John))

(note the difference between __ and _ - there is no rease to assume that this is the same variable)

but again - how to make the final step? forall is again used here and there is no place for John and function number 1?

I am aware that http://subsell.logic.at/bio-CTC/html/BioFLL.Definitions.html contains Definition EncodeRule that is more complex example how the term of type Closed is formed and therefore that can serve as greate example for my question. Unfortunately, some custom defined syntax is involved here and at present this is too hard example for me. As I skimmed through bio-CTC, then there is not example of terms of type ClosedT or ClosedA, at least I did not managed to find.

Very promising work, because formal semantics of natural language can have many different logics and this framework could be great to encode many of them, but is hard for novice.

De Amorim gave answer here https://stackoverflow.com/questions/51254034/how-to-declare-constant-of-some-inductive-type-in-coq/ but it is not explicit and it says that several additional steps and proofs are required.

Alex

How to declare constant of some inductive type in Coq? stackoverflow.com I am following https://github.com/brunofx86/LL/blob/master/FOLL/LL/SyntaxLL.v and there the inductive type is defined (parametrized Higher Order Abstract Syntax - PHOAS is used here): (** Closed T...