Phase 3: Intelligence — 613 mitzvot, 13 middot, Tzara'at diagnostic
Encode all 613 mitzvot from Rambam's Sefer HaMitzvot (248 positive, 365 prohibitions). Build the 13 Middot of Rabbi Yishmael as Prolog inference predicates for hermeneutical reasoning. Implement Tzara'at multi-stage input validation following Vayikra 13-14. Enhance kushya generation with kal vachomer and shnei ketuvim challenge strategies. Architecture §4 Steps 14-15, 19-20. New files: middot/ — 8 files (master + 7 rule modules) diagnostic/ — 4 files (tzaraat, inspection, quarantine, diagnosis) Modified: mitzvot.pl — 52 → 613 mitzvot relationships.pl — expanded tensions, complements, action domains challenge.pl — middot-based kushya (kal vachomer, shnei ketuvim) Tests: 293 total (184 Prolog, 76 Elixir, 33 Haskell), 0 failures. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Scott KarpandClaude Opus 4.6 committed
1 parent
ae78ed26d1
commit
52837cee18
19 files changed
+2795
-178
No files matched your search
@@ -0,0 +1,353 @@
|
||||
%% middot_test.pl — Tests for the 13 Middot of Rabbi Yishmael.
|
||||
%%
|
||||
%% Phase 3: Hermeneutical inference predicates.
|
||||
|
||||
:- use_module(library(plunit)).
|
||||
:- use_module('../src/middot/middot').
|
||||
:- use_module('../src/middot/kal_vachomer').
|
||||
:- use_module('../src/middot/gezerah_shavah').
|
||||
:- use_module('../src/middot/binyan_av').
|
||||
:- use_module('../src/middot/klal_ufrat').
|
||||
:- use_module('../src/middot/davar_yatza').
|
||||
:- use_module('../src/middot/lamed_inyan').
|
||||
:- use_module('../src/middot/shnei_ketuvim').
|
||||
:- use_module('../src/specification/mitzvot').
|
||||
:- use_module('../src/specification/torah_text').
|
||||
:- use_module('../src/specification/root_meanings').
|
||||
|
||||
%% ============================================================
|
||||
%% MASTER MODULE TESTS
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(middot_master).
|
||||
|
||||
%% All 13 middot are named
|
||||
test(all_thirteen_named) :-
|
||||
findall(N, middah_name(N, _), Numbers),
|
||||
length(Numbers, 13).
|
||||
|
||||
%% all_middot returns a list of 13 names
|
||||
test(all_middot_list) :-
|
||||
all_middot(Middot),
|
||||
length(Middot, 13).
|
||||
|
||||
%% Key middot names are correct
|
||||
test(middah_1_is_kal_vachomer) :-
|
||||
middah_name(1, kal_vachomer).
|
||||
|
||||
test(middah_2_is_gezerah_shavah) :-
|
||||
middah_name(2, gezerah_shavah).
|
||||
|
||||
test(middah_13_is_shnei_ketuvim) :-
|
||||
middah_name(13, shnei_ketuvim).
|
||||
|
||||
%% apply_middah works for rule 1 (kal vachomer)
|
||||
test(apply_middah_1, [nondet]) :-
|
||||
apply_middah(1, shabbat_rest, festival_rest, _Reasoning).
|
||||
|
||||
%% apply_middah works for rule 5 (klal ufrat)
|
||||
test(apply_middah_5, [nondet]) :-
|
||||
apply_middah(5,
|
||||
general(fruit_trees),
|
||||
particular([olive, grape]),
|
||||
narrowed_to([olive, grape], from(fruit_trees))).
|
||||
|
||||
:- end_tests(middot_master).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULE 1: KAL VACHOMER
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(kal_vachomer_tests).
|
||||
|
||||
%% Severity ordering: monetary < physical < capital < divine
|
||||
test(monetary_less_than_physical) :-
|
||||
severity_ordering(monetary, physical).
|
||||
|
||||
test(physical_less_than_capital) :-
|
||||
severity_ordering(physical, capital).
|
||||
|
||||
test(capital_less_than_divine) :-
|
||||
severity_ordering(capital, divine).
|
||||
|
||||
%% Transitive stringency
|
||||
test(monetary_less_than_capital) :-
|
||||
is_more_stringent(monetary, capital).
|
||||
|
||||
test(monetary_less_than_divine) :-
|
||||
is_more_stringent(monetary, divine).
|
||||
|
||||
%% Kal vachomer: shabbat → festival
|
||||
test(shabbat_to_festival) :-
|
||||
kal_vachomer(shabbat_rest, festival_rest, _, definite).
|
||||
|
||||
%% Kal vachomer: monetary → physical compensation
|
||||
test(monetary_to_physical) :-
|
||||
kal_vachomer(compensate_monetary, compensate_physical, _, definite).
|
||||
|
||||
%% Kal vachomer: domain-based derivation
|
||||
test(domain_derivation, [nondet]) :-
|
||||
kal_vachomer(
|
||||
law_in(monetary, _),
|
||||
law_in(physical, _),
|
||||
derived(_, from(monetary), to(physical), kal_vachomer),
|
||||
definite
|
||||
).
|
||||
|
||||
%% Unconditional mitzvah implies conditional
|
||||
test(unconditional_implies_conditional, [nondet]) :-
|
||||
kal_vachomer(
|
||||
mitzvah_applies(1, always),
|
||||
mitzvah_applies(1, when(_)),
|
||||
derived(1, unconditional_implies_conditional, kal_vachomer),
|
||||
definite
|
||||
).
|
||||
|
||||
%% Dayo principle: derived law equals source law
|
||||
test(dayo_principle) :-
|
||||
kal_vachomer:dayo(derived(some_law, _, _, _), some_law).
|
||||
|
||||
:- end_tests(kal_vachomer_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULE 2: GEZERAH SHAVAH
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(gezerah_shavah_tests).
|
||||
|
||||
%% Known gezerah shavah: shabbat ↔ pesach (shemirah)
|
||||
test(shabbat_pesach_shemirah) :-
|
||||
gezerah_shavah(shabbat_keeping, pesach_keeping, _, shin_mem_resh).
|
||||
|
||||
%% Known gezerah shavah: shabbat ↔ circumcision (ot)
|
||||
test(shabbat_circumcision_ot) :-
|
||||
gezerah_shavah(shabbat_sign, circumcision_sign, _, aleph_vav_tav).
|
||||
|
||||
%% Shared keyword: two verses sharing a root link
|
||||
test(shared_keyword_creation, [nondet]) :-
|
||||
shared_keyword(ref(bereishit, 1, 1), ref(bereishit, 1, 27), bet_resh_aleph).
|
||||
|
||||
%% Dynamic gezerah shavah from Torah text
|
||||
test(dynamic_gezerah_shavah, [nondet]) :-
|
||||
gezerah_shavah(ref(bereishit, 1, 1), ref(bereishit, 1, 27), _, bet_resh_aleph).
|
||||
|
||||
:- end_tests(gezerah_shavah_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULES 3-4: BINYAN AV
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(binyan_av_tests).
|
||||
|
||||
%% Binyan av from one verse: source verse establishes domain law
|
||||
%% Using Shemot 20:8 — mitzvah 154 (rest_on_shabbat), root qof_dalet_shin → holiness
|
||||
test(binyan_av_one_verse, [nondet]) :-
|
||||
binyan_av_one(ref(shemot, 20, 8), applies_to_domain(_, _), _).
|
||||
|
||||
%% Binyan av from two verses: common root found
|
||||
test(binyan_av_two_verses, [nondet]) :-
|
||||
binyan_av_two(
|
||||
ref(bereishit, 1, 1),
|
||||
ref(bereishit, 1, 27),
|
||||
general_rule(bet_resh_aleph, creation),
|
||||
bet_resh_aleph
|
||||
).
|
||||
|
||||
%% Unified interface: single verse
|
||||
test(binyan_av_single, [nondet]) :-
|
||||
binyan_av(single_verse(ref(shemot, 20, 8)), _, _).
|
||||
|
||||
%% Unified interface: two verses
|
||||
test(binyan_av_two_unified, [nondet]) :-
|
||||
binyan_av(
|
||||
two_verses(ref(bereishit, 1, 1), ref(bereishit, 1, 27)),
|
||||
_,
|
||||
_
|
||||
).
|
||||
|
||||
%% Common principle extraction
|
||||
test(common_principle_from_list, [nondet]) :-
|
||||
common_principle(
|
||||
[ref(bereishit, 1, 1), ref(bereishit, 1, 27)],
|
||||
bet_resh_aleph,
|
||||
_
|
||||
).
|
||||
|
||||
:- end_tests(binyan_av_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULES 5-8: KLAL UFRAT
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(klal_ufrat_tests).
|
||||
|
||||
%% Rule 5: General then particular narrows
|
||||
test(klal_ufrat_narrows) :-
|
||||
klal_ufrat(
|
||||
general(fruit_trees),
|
||||
particular([olive, grape]),
|
||||
narrowed_to([olive, grape], from(fruit_trees))
|
||||
).
|
||||
|
||||
%% Rule 6: Particular then general expands
|
||||
test(prat_uklal_expands) :-
|
||||
prat_uklal(
|
||||
particular([sheep, cattle]),
|
||||
general(all_livestock),
|
||||
expanded_to(all_livestock, including([sheep, cattle]))
|
||||
).
|
||||
|
||||
%% Rule 7: General-particular-general yields similar
|
||||
test(klal_ufrat_uklal_similar) :-
|
||||
klal_ufrat_uklal(
|
||||
general(all_damage),
|
||||
particular([ox_damage, pit_damage, fire_damage]),
|
||||
general(all_damage),
|
||||
similar_to([ox_damage, pit_damage, fire_damage],
|
||||
within(all_damage, negligence_based_damage))
|
||||
).
|
||||
|
||||
%% Generic klal ufrat
|
||||
test(generic_klal_ufrat) :-
|
||||
klal_ufrat(
|
||||
general(any_category),
|
||||
particular(specific_thing),
|
||||
narrowed_to(specific_thing, from(any_category))
|
||||
).
|
||||
|
||||
%% Scope results
|
||||
test(scope_narrowed) :-
|
||||
scope_result(klal_then_prat, narrowed).
|
||||
|
||||
test(scope_expanded) :-
|
||||
scope_result(prat_then_klal, expanded).
|
||||
|
||||
test(scope_similar) :-
|
||||
scope_result(klal_prat_klal, similar).
|
||||
|
||||
:- end_tests(klal_ufrat_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULES 9-11: DAVAR YATZA
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(davar_yatza_tests).
|
||||
|
||||
%% Rule 9: Exception teaches about the general
|
||||
test(exception_teaches_general) :-
|
||||
davar_yatza_llamed(
|
||||
exception(chatat, blood_sprinkling_north),
|
||||
general(all_offerings),
|
||||
teaches(blood_sprinkling_north, applies_to_all(all_offerings))
|
||||
).
|
||||
|
||||
%% Generic rule 9
|
||||
test(generic_exception_teaches) :-
|
||||
davar_yatza_llamed(
|
||||
exception(item, some_law),
|
||||
general(category),
|
||||
teaches(some_law, applies_to_all(category))
|
||||
).
|
||||
|
||||
%% Rule 10: Same type reduces severity
|
||||
test(same_type_reduces) :-
|
||||
davar_yatza_toan_echad(
|
||||
exception(item, shared_law),
|
||||
general(category, shared_law),
|
||||
reduces(shared_law, for(category), because(item))
|
||||
).
|
||||
|
||||
%% Rule 11: Different type creates dual application
|
||||
test(different_type_dual_rules) :-
|
||||
davar_yatza_toan_acher(
|
||||
exception(metzora, outside_camp_procedure),
|
||||
general(tumah, standard_purification),
|
||||
dual_rules(metzora, follows(standard_purification), and(outside_camp_procedure))
|
||||
).
|
||||
|
||||
:- end_tests(davar_yatza_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULE 12: LAMED INYAN
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(lamed_inyan_tests).
|
||||
|
||||
%% "Lo tignov" in context of capital crimes = kidnapping
|
||||
test(lo_tignov_kidnapping) :-
|
||||
lamed_me_inyano(
|
||||
ref(shemot, 20, 15),
|
||||
context(capital_crimes_sequence),
|
||||
meaning(lo_tignov, refers_to(kidnapping), not(ordinary_theft))
|
||||
).
|
||||
|
||||
%% Context from surrounding verses (requires prev and next verse to exist)
|
||||
test(context_from_surrounding, [nondet]) :-
|
||||
lamed_me_inyano(
|
||||
ref(shemot, 20, 14),
|
||||
context(ref(shemot, 20, 13), ref(shemot, 20, 15)),
|
||||
meaning_from(context, ref(shemot, 20, 14))
|
||||
).
|
||||
|
||||
%% Lamed misofo: conclusion clarifies ambiguous topic
|
||||
test(conclusion_clarifies) :-
|
||||
lamed_misofo(
|
||||
ambiguous(topic),
|
||||
concludes_with(clarification),
|
||||
meaning(topic, clarified_by(clarification))
|
||||
).
|
||||
|
||||
%% Unified context_determines_meaning
|
||||
test(context_determines_surrounding, [nondet]) :-
|
||||
context_determines_meaning(
|
||||
ref(shemot, 20, 15),
|
||||
surrounding,
|
||||
meaning(lo_tignov, refers_to(kidnapping), not(ordinary_theft))
|
||||
).
|
||||
|
||||
:- end_tests(lamed_inyan_tests).
|
||||
|
||||
|
||||
%% ============================================================
|
||||
%% RULE 13: SHNEI KETUVIM
|
||||
%% ============================================================
|
||||
|
||||
:- begin_tests(shnei_ketuvim_tests).
|
||||
|
||||
%% Domains in tension
|
||||
test(judgment_mercy_tension) :-
|
||||
domains_in_tension(judgment, mercy).
|
||||
|
||||
test(mercy_judgment_tension) :-
|
||||
domains_in_tension(mercy, judgment).
|
||||
|
||||
test(holiness_transgression_tension) :-
|
||||
domains_in_tension(holiness, transgression).
|
||||
|
||||
%% Two verses with roots in opposing domains contradict
|
||||
test(verses_contradict_detection, [nondet]) :-
|
||||
verses_contradict(V1, V2, domain_conflict(_, _)),
|
||||
V1 \= V2.
|
||||
|
||||
%% Resolving verse shares roots with both
|
||||
test(resolving_verse_found, [nondet]) :-
|
||||
resolving_verse(V1, V2, V3),
|
||||
V1 \= V3,
|
||||
V2 \= V3.
|
||||
|
||||
%% Shnei ketuvim unified interface — harmonized case
|
||||
test(shnei_ketuvim_harmonized, [nondet]) :-
|
||||
shnei_ketuvim(
|
||||
contradicting(V1, V2),
|
||||
harmonized_reading(V1, V2, _V3),
|
||||
reasoning(V1, contradicts(V2), resolved_by(_)),
|
||||
_
|
||||
).
|
||||
|
||||
:- end_tests(shnei_ketuvim_tests).
|
||||
Reference in new issue
Block a user