28 views

Skip to first unread message

Jan 26, 2019, 7:31:39 PM1/26/19

to Abella

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

Jan 26, 2019, 11:39:03 PM1/26/19

to Abella

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.

Jan 27, 2019, 1:40:22 PM1/27/19

to Abella

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 formalizingclassicallinear 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 ofintuitionisticlinear 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.

Jan 28, 2019, 1:05:53 AM1/28/19

to Abella

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

Jan 28, 2019, 4:13:35 AM1/28/19

to Abella

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

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.

Jan 28, 2019, 2:44:25 PM1/28/19

to Abella

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.

Jan 28, 2019, 2:50:14 PM1/28/19

to Abella

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

Jan 28, 2019, 10:22:24 PM1/28/19

to Gopalan Nadathur, abella-the...@googlegroups.com

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

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu