Encoding substructurality

[Siva Somayyajula]

Hi all,

The work on formalizing classical linear logic in Abella (see here) presents it as a sequent calculus, with contexts as lists of hypotheses, in the reasoning logic.

On the other hand, if I were to encode e.g. some fragment of intuitionistic linear logic, I could do it Twelf-style as a linear lambda calculus enforcing linear/exact-once use of hypotheses as a relation over abstractions.

Is there an approach similar to the LJ case study, where the proof system is written in the specification logic, but `{L |- conc C}` "uses" hypotheses in `L` linearly? I'm still trying to wrap my head around how contexts can be manipulated in Abella.

Thanks,

Siva

[Kaustuv Chaudhuri]

Since the specification logic in Abella is not linear, you cannot write a spec that depends on assumptions being used linearly.[1]

If you remain in the reasoning logic to define your provability relation, like the ll-meta proofs so far, then there is no problem at all with linearly. ILL will be conceptually no harder than two-sided classical LL which is already done a bit in the ll-meta proofs.

In the future Abella is probably going to evolve to have some kind of linear specification langauge. However, I am not sure what the timeline on that is. I know of multiple people who are working on it.

Kaustuv

[1] At least there is no simple way to do it. Reed and Pfenning have proposed an alternative way to encode substructural logics using vanilla intuitionistic logic by reifying the substructural properties as side conditions. Frank may be able to tell you what is the best thing to read regarding the current status of this work.

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

[Siva Somayyajula]

Thanks for the response; I'm looking forward to linear specs! I kept the provability relation in the spec logic, but I thread through a context as a list of hypotheses, like this (e.g. linear implication):

proves G (-o A B)      :- proves (A :: G) B.
proves (-o A B :: G) C :- append G1 G2 G, proves G1 A, proves (B :: G2) C.

On Saturday, January 26, 2019 at 11:39:03 PM UTC-5, Kaustuv Chaudhuri wrote:

Since the specification logic in Abella is not linear, you cannot write a spec that depends on assumptions being used linearly.[1]

If you remain in the reasoning logic to define your provability relation, like the ll-meta proofs so far, then there is no problem at all with linearly. ILL will be conceptually no harder than two-sided classical LL which is already done a bit in the ll-meta proofs.

In the future Abella is probably going to evolve to have some kind of linear specification langauge. However, I am not sure what the timeline on that is. I know of multiple people who are working on it.

Kaustuv

[1] At least there is no simple way to do it. Reed and Pfenning have proposed an alternative way to encode substructural logics using vanilla intuitionistic logic by reifying the substructural properties as side conditions. Frank may be able to tell you what is the best thing to read regarding the current status of this work.

On Sun, Jan 27, 2019 at 1:31 AM Siva Somayyajula <siva.som...@gmail.com> wrote:

Hi all,

The work on formalizing classical linear logic in Abella (see here) presents it as a sequent calculus, with contexts as lists of hypotheses, in the reasoning logic.

On the other hand, if I were to encode e.g. some fragment of intuitionistic linear logic, I could do it Twelf-style as a linear lambda calculus enforcing linear/exact-once use of hypotheses as a relation over abstractions.

Is there an approach similar to the LJ case study, where the proof system is written in the specification logic, but `{L |- conc C}` "uses" hypotheses in `L` linearly? I'm still trying to wrap my head around how contexts can be manipulated in Abella.

Thanks,

Siva

--
You received this message because you are subscribed to the Google Groups "Abella" group.

To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-prover+unsub...@googlegroups.com.

[Kaustuv Chaudhuri]

On Sun, Jan 27, 2019 at 7:40 PM Siva Somayyajula <siva.som...@gmail.com> wrote:

I kept the provability relation in the spec logic, but I thread through a context as a list of hypotheses, like this (e.g. linear implication):

proves G (-o A B)      :- proves (A :: G) B.
proves (-o A B :: G) C :- append G1 G2 G, proves G1 A, proves (B :: G2) C.

You can do this, of course, but in that case I am puzzled about what it has to do with your original question. Can you explain precisely what theorem(s) you want to prove?

Kaustuv

[Dale Miller]

On Sunday, January 27, 2019 at 7:40:22 PM UTC+1, Siva Somayyajula wrote:

Thanks for the response; I'm looking forward to linear specs! I kept the provability relation in the spec logic, but I thread through a context as a list of hypotheses, like this (e.g. linear implication):

I look forward to seeing the { |- } construction in Abella evolve to include full linear logic.

In the days before Abella and the nabla quantifier, McDowell and I used the two-level logic approach with a linear logic specification language.  You can find what we wrote about (a subset of) linear logic in Section 5 of the paper

Reasoning with Higher-Order Abstract Syntax in a Logical Framework, by Raymond McDowell and Dale Miller. ACM Transactions on Computational Logic, 3(1) (January 2002), 80 - 136.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf

Since this was before nabla, the encoding is quite complex when dealing with quantifiers in the specification logic.  But the propositional logic aspects might be relevant to what you needed.  When you see the expression  (seq L G) in that paper, think to {L |- G} in Abella.

[Siva Somayyajula]

The reason I didn't define this in the reasoning logic is that I want to execute the proof search that underlies the definition of `proves` as a logic program. Since I also want to prove properties about `proves` like identity reduction, I was wondering if using spec sequents would simplify the process, hence the original question.

The whole story (which is somewhat related) is that once I have the definition of `proves` down, I can extend it to record its derivation process as a "proof certificate" (e.g. a linear lambda calculus term) and write a logic program that relates it to a term of the pi-calculus, recalling that linear logic propositions correspond to session types.

[Siva Somayyajula]

Thanks for the link! I'll check it out.

[Dan DaCosta]

Siva:

I am working towards a modification of Abella that permits reasoning about linear logic specifications. In particular, I want to provide an atomic judgement of the form { P ; D  |- G } to be interpreted as a linear logic judgement. In this judgement, D and G are linear assumptions and goals, respectively. Case analysis on such judgements can get tricky; you have to consider all the ways such a judgement could have been derived and this means considering all the ways linear assumptions and goals could have been partitioned. My focus, in this part of the work, is on determining an effective way of managing such analyses.

Thanks!

Dan DaCosta

On Sun, Jan 27, 2019 at 7:53 AM Gopalan Nadathur <ngop...@umn.edu> wrote:

Dan DaCosta is in fact developing a dissertation at the University of Minnesota that is aimed at enabling the use of linear logic as a specification logic within the Abella system. He will probably have more to say on the topic.

-Gopalan