Skip to content

Commit fbe2ce4

Browse files
committed
Add the PA rule from Liz Coppock's Semantics Boot Camp
This is very similar to the existing lambda notebook PA rule, but works completely syntactically and so is even simpler. It's designed to work in a presuppositional composition system. To swap this in, you can use: lang.set_system(lang.td_presup) lang.get_system().remove_rule("PA") lang.get_system().add_rule(lang.BinaryCompositionOp("PA", lang.sbc_pa, allow_none=True))
1 parent 39a0250 commit fbe2ce4

File tree

3 files changed

+70
-163
lines changed

3 files changed

+70
-163
lines changed

lamb/lang.py

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2509,7 +2509,16 @@ def presup_pa(binder, content, assignment=None):
25092509
f = meta.LFun(types.type_e, content.content.calculate_partiality({bound_var}).under_assignment(new_a), outer_vname)
25102510
return BinaryComposite(binder, content, f)
25112511

2512-
2512+
# this is a presuppositional PA based on Liz Coppock's Semantics Boot Camp
2513+
# PA rule.
2514+
def sbc_pa(binder, content, assignment=None):
2515+
if (binder.content is not None) or not binder.name.strip().isnumeric():
2516+
raise TypeMismatch(binder, content, "Predicate Abstraction")
2517+
index = int(binder.name.strip())
2518+
vname = "var%i" % index
2519+
bound_var = meta.term(vname, types.type_e)
2520+
f = meta.LFun(types.type_e, content.content.calculate_partiality({bound_var}), vname)
2521+
return BinaryComposite(binder, content, f)
25132522

25142523

25152524
def setup_type_driven():

0 commit comments

Comments
 (0)