13 September 2018

LSV library, 9:30-12:00

Agenda:

• Adding injective symbols / conditional rewriting
• Remove brackets?
• Comparison of performances between Lambdapi and Dedukti (Rodolphe)
• Compatibility between Lambdapi and Dedukti (WHNF for example)
• Future syntax of Lambdapi (Rodolphe and Frédéric)
• Characters allowed in symbol names (Why /,+,*,%,=,@... are not allowed?) (Guillaume G.)
• Point on termination checker (G. Genestier)
• Point on Lambdapi user interface (Emilio?)
• Point on Lambdapi tactics (Aris and Franck)
• A new typing algorithm for rewrite rules to prove subject reduction
• When do we do the next release? Which new features do we add (polarized rewrite rules, AC, export termination problem file)?
• Non-terminating file in the iProver library (Guillaume G., Rodolphe)

Speed: Lambdapi and Dedukti

See https://github.com/rlepigre/lambdapi/blob/master/PERFS.md

• Lambdapi and Dedukti are quite similar. Sometimes Lambdapi is better than Dedukti (30% for Focalide and VerInE). For the other libraries Dedukti is better. However, the Zenon library is really faster to check in Dedukti than in Lambdapi. It remains to investigate the reasons for these results.
• It would be nice compare Lambdapi and Dedukti on Matita without the unique file that takes so long.

Compatibility between Lambdapi and Dedukti

• Libraries should be updated so that the command "#REQUIRE" becomes mandatory.
• #EVAL[WHNF] will stay different

Ideas of internship

• Everyone should think of possible subjects
• Decision trees for lambdapi
• Misfix operators for lambdapi (not urgent)
• Rewriting modulo AC in Lambdapi
• injectivity
• conditional rewriting

New syntax

A file was presented by Rodolphe:

See https://github.com/rlepigre/lambdapi/blob/new_parser/new_syntax.bnf

• Should we force Unicode?
• Should we use Unicode for identifiers?
• Arrows symbols: What should you use?
• Left parameters for theorems? (mathcomp) YES
• definition with tactics?
• No misfix operator
• KIND in the syntax

Brackets

• Ask Raphaël for a concrete example, but they will be removed

Injective symbols

• Added in Dedukti

Conditional Rewriting

• We keep it as a PR + we add a parser for a competition